×

Incremental bounded model checking for embedded software. (English) Zbl 1375.68081


MSC:

68Q60 Specification and verification (program logics, model checking, etc.)
PDFBibTeX XMLCite
Full Text: DOI arXiv

References:

[1] Alur R, Kanade A, Ramesh S, Shashidhar KC (2008) Symbolic analysis for improving simulation coverage of Simulink/Stateflow models. In: International conference on embedded software. ACM, pp 89-98 · Zbl 1159.68403
[2] Brummayer R, Biere A (2009) Boolector: an efficient SMT solver for bit-vectors and arrays. In: Tools and algorithms for the construction and analysis of systems. Springer, Berlin, pp 174-177 · Zbl 1187.68168
[3] Brummayer R, Biere A (2009) Lemmas on demand for the extensional theory of arrays. J Satisf Boolean Model Comput 6(1-3): 165-201 · Zbl 1187.68168
[4] Brummayer R, Biere A (2009) Effective bit-width and under-approximation. In: Computer aided systems theory. Springer, Berlin, pp 304-311
[5] Biere A, Cimatti A, Clarke EM, Zhu Y (1999) Symbolic model checking without BDDs. In: Tools and algorithms for the construction and analysis of systems. Springer, Berlin, pp 193-207
[6] Beyer D, Dangl M, Wendler P (2015) Boosting k-induction with continuously-refined invariants. In Computer-aided verification. Springer, Berlin, pp 622-640
[7] Biere A (2008) PicoSAT essentials. J Satisf Boolean Model Comput 4(2-4): 75-97 · Zbl 1159.68403
[8] Brain M, Joshi S, Kroening D, Schrammel P (2015) Safety verification and refutation by k-invariants and k-induction. In: Static analysis symposium. Springer, Berlin, pp 145-161
[9] Bryant RE, Kroening D, Ouaknine J, Seshia SA, Strichman O, Brady BA (2007) Deciding bit-vector arithmetic with abstraction. In: Tools and algorithms for the construction and analysis of systems. Springer, Berlin, pp 358-372 · Zbl 1186.68281
[10] Bryant RE, Kroening D, Ouaknine J, Seshia SA, Strichman O, Brady BA (2009) An abstraction-based decision procedure for bit-vector arithmetic. J Softw Tools Technol Transf 11(2): 95-104 · Zbl 1186.68281 · doi:10.1007/s10009-009-0101-x
[11] Brillout A, Kroening D, Wahl T (2009) Mixed abstractions for floating-point arithmetic. In: Formal methods in computer-aided design. IEEE, pp 69-76
[12] Bradley AR (2012) IC3 and beyond: incremental, inductive verification. In: Computer-aided verification. Springer, Berlin, p 4 · Zbl 1322.68054
[13] Buechi Julius R (1962) On a decision method in restricted second-order arithmetic. In: International congress on logic, methodology, and philosophy of science. Stanford University Press, Stanford, pp 1-11 · Zbl 0787.68049
[14] Clarke E, Biere A, Raimi R, Zhu Y (2001) Bounded model checking using satisfiability solving. Form Methods Syst Des 19(1): 7-34 · Zbl 0985.68038 · doi:10.1023/A:1011276507260
[15] Cadar C, Dunbar D, Engler DR (2008) KLEE: unassisted and automatic generation of high-coverage tests for complex systems programs. In: Operating systems design and implementation. USENIX Association, pp 209-224
[16] Clarke EM, Kroening D, Lerda F (2004) A tool for checking ANSI-C programs. In: Tools and algorithms for the construction and analysis of systems. Springer, Berlin, pp 168-176 · Zbl 1126.68470
[17] Cimatti A, Micheli A, Narasamdya I, Roveri M (2010) Verifying SystemC: a software model checking approach. In: Form Methods Comput Aided Des. IEEE, pp 51-59 · Zbl 0787.68049
[18] Chakraborty S, Ramesh S, Teich J (2010) Model-based analysis, synthesis and testing of automotive hardware/software architectures. In: International conference on embedded software. ACM, pp 299-300
[19] Dias Neto AC, Horta Travassos G (2010) A picture from the model-based testing area: concepts, techniques, and challenges. Adv Comput 80: 45-120 · doi:10.1016/S0065-2458(10)80002-6
[20] Donaldson A, Haller L, Kroening D, Rümmer P (2011) Software verification using k-induction. In: Static analysis symposium. Springer, Berlin, pp 351-368
[21] Eén N, Mishchenko A, Amla N (2010) A single-instance incremental SAT formulation of proof- and counterexample-based abstraction. In: Formal methods in computer-aided design. IEEE, pp 181-188 · Zbl 0985.68038
[22] Eén N, Mishchenko A, Brayton RK (2011) Efficient implementation of property directed reachability. In: Formal Methods in Computer-Aided Design. IEEE, pp 125-134
[23] Eén N, Sörensson N (2003) An extensible SAT-solver. In: Theory and applications of satisfiability testing. Springer, Berlin, pp 502-518 · Zbl 1204.68191
[24] Eén N, Sörensson N (2003) Temporal induction by incremental SAT solving. Electron Notes Theor Comput Sci 89: 4-543560 · Zbl 1271.68215 · doi:10.1016/S1571-0661(05)82542-3
[25] Fleming P, Wallace J (1986) How not to lie with statistics: the correct way to summarize benchmark results. Commun ACM, 29(3): 218-221 · doi:10.1145/5666.5673
[26] Fraser G, Wotawa F, Ammann P (2009) Testing with model checkers: a survey. Softw Test Verif Reliab 19(3): 215-261 · doi:10.1002/stvr.402
[27] Gunnarsson D, Kuntz S, Farrall G, Iwai A, Ernst R (2012) Trends in automotive embedded systems. In: International conference on hardware/software codesign and system synthesis. IEEE, pp 9-10 · Zbl 1271.68215
[28] Günther H, Weissenbacher G (2014) Incremental bounded software model checking. ACM, pp 40-47
[29] Halbwachs N (1993) Synchronous programming of reactive systems. Kluwer · Zbl 0828.68038
[30] Harman M, Hierons RM (2001) An overview of program slicing. Softw Focus 2(3): 85-92 · doi:10.1002/swf.41
[31] He N, Hsiao MS (2008) A new testability guided abstraction to solving bit-vector formula. In: International workshop on bit-precise reasoning
[32] Hooker JN (1993) Solving the incremental satisfiability problem. J Log Algebraic Program 15(1&2): 177-186 · Zbl 0787.68049 · doi:10.1016/0743-1066(93)90018-C
[33] Herber P, Reicherdt R, Bittner P (2013) Bit-precise formal verification of discrete-time MATLAB/Simulink models using SMT solving. In: International conference on embedded software, pp 1-10
[34] Holzer A, Schallhart C, Tautschnig M, Veith H (2009) Query-driven program testing. In: Verification, model checking, and abstract interpretation. Springer, Berlin, pp 151-166 · Zbl 1206.68089
[35] Hagen G, Tinelli C (2008) Scaling up the formal verification of Lustre programs with SMT-based techniques. In: Formal methods in computer-aided design. IEEE, pp 1-9
[36] Hayhurst KJ, Veerhusen DS, Chilenski JJ, Rierson LK (2001) A practical tutorial on modified condition/decision coverage. Technical report, NASA
[37] ISO 26262: Road vehicles—functional safety (2011)
[38] Inverso O, Tomasco E, Fischer B, La Torre S, Parlato G (2014) Bounded model checking of multi-threaded C programs via lazy sequentialization. In: Computer-aided verification. Springer, Berlin, pp 585-602
[39] Jin H, Somenzi F (2005) An incremental algorithm to check satisfiability for bounded model checking. Electron Notes Theor Comput Sci 119: 2-5165 · Zbl 1272.68262 · doi:10.1016/j.entcs.2004.06.062
[40] Kroening D, Lewis M, Weissenbacher G (2015) Under-approximating loops in C programs for fast counterexample detection. Form Methods Syst Des 47(1): 75-92 · Zbl 1322.68054 · doi:10.1007/s10703-015-0228-1
[41] Kroening D, Ouaknine J, Strichman O, Wahl T, Worrell J (2011) Linear completeness thresholds for bounded model checking. In: Computer-aided verification. Springer, pp 557-572 · Zbl 1360.68592
[42] Kroening D, Strichman O (2003) Efficient computation of recurrence diameters. In: Verification, model checking, and abstract interpretation. Springer, Berlin, pp 298-309 · Zbl 1022.68579
[43] Kroening D, Tautschnig M (2014) CBMC—C bounded model checker—(competition contribution). In: Tools and algorithms for the construction and analysis of systems. Springer, Berlin, pp 389-391
[44] Kim J, Whittemore J, Sakallah KA, Marques Silva JP (2000) On applying incremental satisfiability to delay fault testing. In: Design automation and test in Europe. IEEE, pp 380-384
[45] Manamcheri K, Mitra S, Bak S, Caccamo M (2011) A step towards verification and synthesis from simulink/stateflow models. In: Hybrid systems: computation and control. ACM, pp 317-318
[46] Petrenko A, daSilva Simão A, Maldonado JC (2012) Model-based testing of software and systems: recent advances and challenges. J Softw Tools Technol Transf 14(4): 383-386 · doi:10.1007/s10009-012-0240-3
[47] Peranandam P, Raviram S, Satpathy M, Yeolekar A, Gadkari AA, Ramesh S (2012) An integrated test generation tool for enhanced coverage of simulink/stateflow models. In: Design automation and test in Europe. IEEE, pp 308-311
[48] Pnueli A, Strichman O (2006) Reduced functional consistency of uninterpreted functions. Electron Notes Theor Comput Sci 144(2): 53-65 · Zbl 1272.03071 · doi:10.1016/j.entcs.2005.12.006
[49] Schrammel P, Kroening D (2016) 2LS for program analysis—(competition contribution). In: Tools and algorithms for the construction and analysis of systems. Springer, Berlin, pp 905-907
[50] Schrammel P, Kroening D, Brain M, Martins R, Teige T, Bienmüller T (2015) Successful use of incremental BMC in the automotive industry. In: Formal methods for industrial critical systems. Springer, Berlin, pp 62-76
[51] Silva JM, Sakallah KA (1997) Robust search algorithms for test pattern generation. IEEE, pp 152-161 · Zbl 1272.68262
[52] Sheeran M, Singh S, Stålmarck G (2000) Checking safety properties using induction and a SAT-solver. In: Formal methods in computer-aided design, volume 1954 of LNCS. IEEE, pp 108-125
[53] Stump A, Sutcliffe G, Tinelli C (2014) StarExec: a cross-community infrastructure for logic solving. In: International joint conference on automated reasoning, pp 367-373 · Zbl 06348250
[54] Strichman O (2001) Pruning techniques for the SAT-based bounded model checking problem. Springer, Berlin, pp 58-70 · Zbl 1002.68511
[55] Satpathy M, Yeolekar A, Ramesh S (2008) Randomized directed testing (REDIRECT) for simulink/stateflow models. In: International conference on embedded software, pp 217-226
[56] Tip F (1994) A survey of program slicing techniques. Technical report, CWI-Amsterdam · Zbl 0806.47066
[57] Wieringa S (2011) On incremental satisfiability and bounded model checking. In: Design and implementation of formal tools and systems, pp 46-54
[58] Whittemore J, Kim J, Sakallah KA (2001) SATIRE: a new incremental satisfiability engine. In: Design automation conference. ACM, pp 542-545
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.