{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,27]],"date-time":"2025-10-27T10:50:08Z","timestamp":1761562208695,"version":"3.37.3"},"reference-count":58,"publisher":"Association for Computing Machinery (ACM)","issue":"5","license":[{"start":{"date-parts":[[2017,9,1]],"date-time":"2017-09-01T00:00:00Z","timestamp":1504224000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"name":"ARTEMIS JU","award":["280053"],"award-info":[{"award-number":["280053"]}]},{"name":"ERC","award":["295311"],"award-info":[{"award-number":["295311"]}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[2017,9]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>\n            Program analysis is on the brink of mainstream usage in embedded systems development. Formal verification of behavioural requirements, finding runtime errors and test case generation are some of the most common applications of automated verification tools based on bounded model checking (BMC). Existing industrial tools for embedded software use an off-the-shelf bounded model checker and apply it iteratively to verify the program with an increasing number of unwindings. This approach unnecessarily wastes time repeating work that has already been done and fails to exploit the power of incremental SAT solving. This article reports on the extension of the software model checker C\n            <jats:sc>BMC<\/jats:sc>\n            to support\n            <jats:italic>incremental BMC<\/jats:italic>\n            and its successful integration with the industrial embedded software verification tool BTC E\n            <jats:sc>MBEDDED<\/jats:sc>\n            <jats:sc>TESTER<\/jats:sc>\n            . We present an extensive evaluation over large industrial embedded programs, mainly from the automotive industry. We show that incremental BMC cuts runtimes by\n            <jats:italic>one order of magnitude<\/jats:italic>\n            in comparison to the standard non-incremental approach, enabling the application of formal verification to large and complex embedded software. We furthermore report promising results on analysing programs with arbitrary loop structure using incremental BMC, demonstrating its applicability and potential to verify general software beyond the embedded domain.\n          <\/jats:p>","DOI":"10.1007\/s00165-017-0419-1","type":"journal-article","created":{"date-parts":[[2017,2,22]],"date-time":"2017-02-22T08:04:41Z","timestamp":1487750681000},"page":"911-931","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":20,"title":["Incremental bounded model checking for embedded software"],"prefix":"10.1145","volume":"29","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-5713-1381","authenticated-orcid":false,"given":"Peter","family":"Schrammel","sequence":"first","affiliation":[{"name":"School of Engineering and Informatics, University of Sussex, BN1 9RH, Brighton, UK"},{"name":"Department of Computer Science, University of Oxford, Oxford, UK"}]},{"given":"Daniel","family":"Kroening","sequence":"additional","affiliation":[{"name":"Department of Computer Science, University of Oxford, Oxford, UK"}]},{"given":"Martin","family":"Brain","sequence":"additional","affiliation":[{"name":"Department of Computer Science, University of Oxford, Oxford, UK"}]},{"given":"Ruben","family":"Martins","sequence":"additional","affiliation":[{"name":"Department of Computer Science, University of Oxford, Oxford, UK"},{"name":"Department of Computer Science, University of Texas at Austin, Austin, USA"}]},{"given":"Tino","family":"Teige","sequence":"additional","affiliation":[{"name":"BTC Embedded Systems AG, Oldenburg, Germany"}]},{"given":"Tom","family":"Bienm\u00fcller","sequence":"additional","affiliation":[{"name":"BTC Embedded Systems AG, Oldenburg, Germany"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","doi-asserted-by":"crossref","unstructured":"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\u201398","DOI":"10.1145\/1450058.1450071"},{"key":"e_1_2_1_2_2_2","doi-asserted-by":"crossref","unstructured":"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\u2013177","DOI":"10.1007\/978-3-642-00768-2_16"},{"issue":"1","key":"e_1_2_1_2_3_2","first-page":"165","article-title":"Lemmas on demand for the extensional theory of arrays","volume":"6","author":"Brummayer R","year":"2009","journal-title":"J Satisf Boolean Model Comput"},{"key":"e_1_2_1_2_4_2","doi-asserted-by":"crossref","unstructured":"Brummayer R Biere A (2009) Effective bit-width and under-approximation. In: Computer aided systems theory. Springer Berlin pp 304\u2013311","DOI":"10.1007\/978-3-642-04772-5_40"},{"key":"e_1_2_1_2_5_2","doi-asserted-by":"crossref","unstructured":"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\u2013207","DOI":"10.1007\/3-540-49059-0_14"},{"key":"e_1_2_1_2_6_2","doi-asserted-by":"crossref","unstructured":"Beyer D Dangl M Wendler P (2015) Boosting k-induction with continuously-refined invariants. In Computer-aided verification. Springer Berlin pp 622\u2013640","DOI":"10.1007\/978-3-319-21690-4_42"},{"issue":"2","key":"e_1_2_1_2_7_2","first-page":"75","article-title":"PicoSAT essentials","volume":"4","author":"Biere A","year":"2008","journal-title":"J Satisf Boolean Model Comput"},{"key":"e_1_2_1_2_8_2","doi-asserted-by":"crossref","unstructured":"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\u2013161","DOI":"10.1007\/978-3-662-48288-9_9"},{"key":"e_1_2_1_2_9_2","doi-asserted-by":"crossref","unstructured":"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\u2013372","DOI":"10.1007\/978-3-540-71209-1_28"},{"key":"e_1_2_1_2_10_2","doi-asserted-by":"publisher","DOI":"10.5555\/3220882.3220984"},{"key":"e_1_2_1_2_11_2","doi-asserted-by":"crossref","unstructured":"Brillout A Kroening D Wahl T (2009) Mixed abstractions for floating-point arithmetic. In: Formal methods in computer-aided design. IEEE pp 69\u201376","DOI":"10.1109\/FMCAD.2009.5351141"},{"key":"e_1_2_1_2_12_2","doi-asserted-by":"crossref","unstructured":"Bradley AR (2012) IC3 and beyond: incremental inductive verification. In: Computer-aided verification. Springer Berlin p 4","DOI":"10.1007\/978-3-642-31424-7_4"},{"key":"e_1_2_1_2_13_2","unstructured":"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\u201311"},{"key":"e_1_2_1_2_14_2","doi-asserted-by":"publisher","DOI":"10.1023\/A:1011276507260"},{"key":"e_1_2_1_2_15_2","unstructured":"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\u2013224"},{"key":"e_1_2_1_2_16_2","doi-asserted-by":"crossref","unstructured":"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\u2013176","DOI":"10.1007\/978-3-540-24730-2_15"},{"key":"e_1_2_1_2_17_2","unstructured":"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\u201359"},{"key":"e_1_2_1_2_18_2","doi-asserted-by":"crossref","unstructured":"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\u2013300","DOI":"10.1145\/1879021.1879061"},{"key":"e_1_2_1_2_19_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0065-2458(10)80002-6"},{"key":"e_1_2_1_2_20_2","doi-asserted-by":"crossref","unstructured":"Donaldson A Haller L Kroening D R\u00fcmmer P (2011) Software verification using k -induction. In: Static analysis symposium. Springer Berlin pp 351\u2013368","DOI":"10.1007\/978-3-642-23702-7_26"},{"key":"e_1_2_1_2_21_2","unstructured":"E\u00e9n 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\u2013188"},{"key":"e_1_2_1_2_22_2","unstructured":"E\u00e9n N Mishchenko A Brayton RK (2011) Efficient implementation of property directed reachability. In: Formal Methods in Computer-Aided Design. IEEE pp 125\u2013134"},{"key":"e_1_2_1_2_23_2","doi-asserted-by":"crossref","unstructured":"E\u00e9n N S\u00f6rensson N (2003) An extensible SAT-solver. In: Theory and applications of satisfiability testing. Springer Berlin pp 502\u2013518","DOI":"10.1007\/978-3-540-24605-3_37"},{"key":"e_1_2_1_2_24_2","first-page":"4","article-title":"Temporal induction by incremental SAT solving","volume":"89","author":"E\u00e9n N","year":"2003","journal-title":"Electron Notes Theor Comput Sci"},{"key":"e_1_2_1_2_25_2","doi-asserted-by":"publisher","DOI":"10.1145\/5666.5673"},{"key":"e_1_2_1_2_26_2","doi-asserted-by":"publisher","DOI":"10.1002\/stvr.402"},{"key":"e_1_2_1_2_27_2","doi-asserted-by":"crossref","unstructured":"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\u201310","DOI":"10.1145\/2380445.2380452"},{"key":"e_1_2_1_2_28_2","doi-asserted-by":"crossref","unstructured":"G\u00fcnther H Weissenbacher G (2014) Incremental bounded software model checking. ACM pp 40\u201347","DOI":"10.1145\/2632362.2632374"},{"key":"e_1_2_1_2_29_2","doi-asserted-by":"crossref","unstructured":"Halbwachs N (1993) Synchronous programming of reactive systems. Kluwer","DOI":"10.1007\/978-1-4757-2231-4"},{"key":"e_1_2_1_2_30_2","doi-asserted-by":"publisher","DOI":"10.1002\/swf.41"},{"key":"e_1_2_1_2_31_2","doi-asserted-by":"crossref","unstructured":"He N Hsiao MS (2008) A new testability guided abstraction to solving bit-vector formula. In: International workshop on bit-precise reasoning","DOI":"10.1145\/1512464.1512473"},{"key":"e_1_2_1_2_32_2","doi-asserted-by":"publisher","DOI":"10.1016\/0743-1066(93)90018-C"},{"key":"e_1_2_1_2_33_2","doi-asserted-by":"crossref","unstructured":"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\u201310","DOI":"10.1109\/EMSOFT.2013.6658586"},{"key":"e_1_2_1_2_34_2","doi-asserted-by":"crossref","unstructured":"Holzer A Schallhart C Tautschnig M Veith H (2009) Query-driven program testing. In: Verification model checking and abstract interpretation. Springer Berlin pp 151\u2013166","DOI":"10.1007\/978-3-540-93900-9_15"},{"key":"e_1_2_1_2_35_2","doi-asserted-by":"crossref","unstructured":"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\u20139","DOI":"10.1109\/FMCAD.2008.ECP.19"},{"key":"e_1_2_1_2_36_2","unstructured":"Hayhurst KJ Veerhusen DS Chilenski JJ Rierson LK (2001) A practical tutorial on modified condition\/decision coverage. Technical report NASA"},{"key":"e_1_2_1_2_37_2","unstructured":"ISO 26262: Road vehicles\u2014functional safety (2011)"},{"key":"e_1_2_1_2_38_2","doi-asserted-by":"crossref","unstructured":"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\u2013602","DOI":"10.1007\/978-3-319-08867-9_39"},{"key":"e_1_2_1_2_39_2","first-page":"2","article-title":"An incremental algorithm to check satisfiability for bounded model checking","volume":"119","author":"Jin H","year":"2005","journal-title":"Electron Notes Theor Comput Sci"},{"key":"e_1_2_1_2_40_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-015-0228-1"},{"key":"e_1_2_1_2_41_2","doi-asserted-by":"crossref","unstructured":"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\u2013572","DOI":"10.1007\/978-3-642-22110-1_44"},{"key":"e_1_2_1_2_42_2","doi-asserted-by":"crossref","unstructured":"Kroening D Strichman O (2003) Efficient computation of recurrence diameters. In: Verification model checking and abstract interpretation. Springer Berlin pp 298\u2013309","DOI":"10.1007\/3-540-36384-X_24"},{"key":"e_1_2_1_2_43_2","doi-asserted-by":"crossref","unstructured":"Kroening D Tautschnig M (2014) CBMC\u2014C bounded model checker\u2014(competition contribution). In: Tools and algorithms for the construction and analysis of systems. Springer Berlin pp 389\u2013391","DOI":"10.1007\/978-3-642-54862-8_26"},{"key":"e_1_2_1_2_44_2","doi-asserted-by":"crossref","unstructured":"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\u2013384","DOI":"10.1145\/343647.343801"},{"key":"e_1_2_1_2_45_2","doi-asserted-by":"crossref","unstructured":"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\u2013318","DOI":"10.1145\/1967701.1967749"},{"key":"e_1_2_1_2_46_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-012-0240-3"},{"key":"e_1_2_1_2_47_2","doi-asserted-by":"crossref","unstructured":"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\u2013311","DOI":"10.1109\/DATE.2012.6176485"},{"key":"e_1_2_1_2_48_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2005.12.006"},{"key":"e_1_2_1_2_49_2","doi-asserted-by":"crossref","unstructured":"Schrammel P Kroening D (2016) 2LS for program analysis\u2014(competition contribution). In: Tools and algorithms for the construction and analysis of systems. Springer Berlin pp 905\u2013907","DOI":"10.1007\/978-3-662-49674-9_56"},{"key":"e_1_2_1_2_50_2","doi-asserted-by":"crossref","unstructured":"Schrammel P Kroening D Brain M Martins R Teige T Bienm\u00fcller T (2015) Successful use of incremental BMC in the automotive industry. In: Formal methods for industrial critical systems. Springer Berlin pp 62\u201376","DOI":"10.1007\/978-3-319-19458-5_5"},{"key":"e_1_2_1_2_51_2","unstructured":"Silva JM Sakallah KA (1997) Robust search algorithms for test pattern generation. IEEE pp 152\u2013161"},{"key":"e_1_2_1_2_52_2","doi-asserted-by":"crossref","unstructured":"Sheeran M Singh S St\u00e5lmarck 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\u2013125","DOI":"10.1007\/3-540-40922-X_8"},{"key":"e_1_2_1_2_53_2","doi-asserted-by":"crossref","unstructured":"Stump A Sutcliffe G Tinelli C (2014) StarExec: a cross-community infrastructure for logic solving. In: International joint conference on automated reasoning pp 367\u2013373","DOI":"10.1007\/978-3-319-08587-6_28"},{"key":"e_1_2_1_2_54_2","doi-asserted-by":"crossref","unstructured":"Strichman O (2001) Pruning techniques for the SAT-based bounded model checking problem. Springer Berlin pp 58\u201370","DOI":"10.1007\/3-540-44798-9_4"},{"key":"e_1_2_1_2_55_2","doi-asserted-by":"crossref","unstructured":"Satpathy M Yeolekar A Ramesh S (2008) Randomized directed testing (REDIRECT) for simulink\/stateflow models. In: International conference on embedded software pp 217\u2013226","DOI":"10.1145\/1450058.1450088"},{"key":"e_1_2_1_2_56_2","unstructured":"Tip F (1994) A survey of program slicing techniques. Technical report CWI-Amsterdam"},{"key":"e_1_2_1_2_57_2","unstructured":"Wieringa S (2011) On incremental satisfiability and bounded model checking. In: Design and implementation of formal tools and systems pp 46\u201354"},{"key":"e_1_2_1_2_58_2","doi-asserted-by":"crossref","unstructured":"Whittemore J Kim J Sakallah KA (2001) SATIRE: a new incremental satisfiability engine. In: Design automation conference. ACM pp 542\u2013545","DOI":"10.1145\/378239.379019"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00165-017-0419-1\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-017-0419-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-017-0419-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s00165-017-0419-1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,7]],"date-time":"2022-01-07T06:54:54Z","timestamp":1641538494000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s00165-017-0419-1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,9]]},"references-count":58,"journal-issue":{"issue":"5","published-print":{"date-parts":[[2017,9]]}},"alternative-id":["10.1007\/s00165-017-0419-1"],"URL":"https:\/\/doi.org\/10.1007\/s00165-017-0419-1","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"type":"print","value":"0934-5043"},{"type":"electronic","value":"1433-299X"}],"subject":[],"published":{"date-parts":[[2017,9]]}}}