{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,28]],"date-time":"2025-11-28T12:37:53Z","timestamp":1764333473463,"version":"3.40.3"},"publisher-location":"Cham","reference-count":83,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031711763"},{"type":"electronic","value":"9783031711770"}],"license":[{"start":{"date-parts":[[2024,9,13]],"date-time":"2024-09-13T00:00:00Z","timestamp":1726185600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2024,9,13]],"date-time":"2024-09-13T00:00:00Z","timestamp":1726185600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Over the past few years there has been significant progress in the various fields of software verification resulting in many useful tools and successful deployments, both academic and commercial. However much of the work describing these tools and ideas is written by and for the research community. The scale, diversity and focus of the literature can act as a barrier, separating industrial users and the wider academic community from the tools that could make their work more efficient, more certain and more productive. This tutorial gives a simple classification of verification techniques in terms of a pyramid and uses it to describe the six main schools of verification technologies. We have found this approach valuable for building collaborations with industry as it allows us to explain the intrinsic strengths and weaknesses of techniques and pick the right tool for any given industrial application. The model also highlights some of the cultural differences and unspoken assumptions of different areas of verification and illuminates future directions.<\/jats:p>","DOI":"10.1007\/978-3-031-71177-0_24","type":"book-chapter","created":{"date-parts":[[2024,9,12]],"date-time":"2024-09-12T06:10:51Z","timestamp":1726121451000},"page":"393-419","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["A Pyramid Of (Formal) Software Verification"],"prefix":"10.1007","author":[{"given":"Martin","family":"Brain","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Elizabeth","family":"Polgreen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2024,9,13]]},"reference":[{"key":"24_CR1","unstructured":"Coverity Scan: Static analysis. https:\/\/scan.coverity.com\/. Accessed 10 Apr 2024"},{"key":"24_CR2","unstructured":"Cppcheck: A tool for static C\/C++ code analysis. https:\/\/cppcheck.sourceforge.io\/. Accessed 10 Apr 2024"},{"key":"24_CR3","unstructured":"CREST: Concolic test generation tool for C. https:\/\/www.burn.im\/crest\/. Accessed 20 July 2020"},{"key":"24_CR4","unstructured":"FindBugs. http:\/\/findbugs.sourceforge.net\/. Accessed 22 July 2020"},{"key":"24_CR5","unstructured":"Fortify static code analyzer. https:\/\/www.opentext.com\/products\/fortify-static-code-analyzer. Accessed 10 Apr 2024"},{"key":"24_CR6","unstructured":"MALPAS software static analysis toolset. http:\/\/malpas-global.com\/. Accessed 10 Apr 2024"},{"key":"24_CR7","unstructured":"PolySpace Code Prover. https:\/\/www.mathworks.com\/products\/polyspace-code-prover.html. Accessed 22 July 2020"},{"key":"24_CR8","unstructured":"SPARK. https:\/\/www.adacore.com\/about-spark. Accessed 10 Apr 2024"},{"key":"24_CR9","unstructured":"Baier, C., Katoen, J.: Principles of Model Checking. MIT Press (2008)"},{"key":"24_CR10","doi-asserted-by":"crossref","unstructured":"Ball, T., Majumdar, R., Millstein, T.D., Rajamani, S.K.: Automatic predicate abstraction of C programs. In: Burke, M., Soffa, M.L. (eds.) Proceedings of the 2001 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), Snowbird, Utah, USA, June 20-22, 2001, pp. 203\u2013213. ACM (2001)","DOI":"10.1145\/378795.378846"},{"key":"24_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"364","DOI":"10.1007\/11804192_17","volume-title":"Formal Methods for Components and Objects","author":"M Barnett","year":"2006","unstructured":"Barnett, M., Chang, B.Y.E., DeLine, R., Jacobs, B., Leino, K.R.M.: Boogie: a modular reusable verifier for object-oriented programs. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.P. (eds.) FMCO 2005. LNCS, vol. 4111, pp. 364\u2013387. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11804192_17"},{"key":"24_CR12","doi-asserted-by":"publisher","unstructured":"Bertot, Y., Cast\u00e9ran, P.: Interactive Theorem Proving and Program Development: Coq\u2019Art: The Calculus of Inductive Constructions. Texts in Theoretical Computer Science. An EATCS Series. Springer, Berlin, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-662-07964-5","DOI":"10.1007\/978-3-662-07964-5"},{"key":"24_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"184","DOI":"10.1007\/978-3-642-22110-1_16","volume-title":"Computer Aided Verification","author":"D Beyer","year":"2011","unstructured":"Beyer, D., Keremoglu, M.E.: CPAchecker: a tool for configurable software verification. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 184\u2013190. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-22110-1_16"},{"key":"24_CR14","unstructured":"Biere, A.: Bounded model checking. In: Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.) Handbook of Satisfiability, Frontiers in Artificial Intelligence and Applications, vol.\u00a0185, pp. 457\u2013481. IOS Press (2009)"},{"key":"24_CR15","doi-asserted-by":"crossref","unstructured":"Biere, A., Cimatti, A., Clarke, E.M., Fujita, M., Zhu, Y.: Symbolic model checking using SAT procedures instead of BDDs. In: Irwin, M.J. (ed.) Proceedings of the 36th Conference on Design Automation, New Orleans, LA, USA, June 21-25, 1999, pp. 317\u2013320. ACM Press (1999)","DOI":"10.1145\/309847.309942"},{"key":"24_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"70","DOI":"10.1007\/978-3-642-18275-4_7","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"AR Bradley","year":"2011","unstructured":"Bradley, A.R.: SAT-based model checking without unrolling. In: Jhala, R., Schmidt, D. (eds.) VMCAI 2011. LNCS, vol. 6538, pp. 70\u201387. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-18275-4_7"},{"key":"24_CR17","unstructured":"Burch, J.R., Clarke, E.M., McMillan, K.L., Dill, D.L., Hwang, L.J.: Symbolic model checking: 10$$\\hat{\\,}$$20 states and beyond. In: Proceedings of the Fifth Annual Symposium on Logic in Computer Science (LICS \u201990), Philadelphia, Pennsylvania, USA, June 4-7, 1990, pp. 428\u2013439. IEEE Computer Society (1990)"},{"key":"24_CR18","unstructured":"Cadar, C., Dunbar, D., Engler, D.R.: KLEE: unassisted and automatic generation of high-coverage tests for complex systems programs. In: OSDI, pp. 209\u2013224. USENIX Association (2008)"},{"key":"24_CR19","doi-asserted-by":"crossref","unstructured":"Cadar, C., et al.: Symbolic execution for software testing in practice: preliminary assessment. In: ICSE, pp. 1066\u20131071. ACM (2011)","DOI":"10.1145\/1985793.1985995"},{"issue":"2","key":"24_CR20","doi-asserted-by":"publisher","first-page":"82","DOI":"10.1145\/2408776.2408795","volume":"56","author":"C Cadar","year":"2013","unstructured":"Cadar, C., Sen, K.: Symbolic execution for software testing: three decades later. Commun. ACM 56(2), 82\u201390 (2013)","journal-title":"Commun. ACM"},{"issue":"1","key":"24_CR21","doi-asserted-by":"publisher","first-page":"47","DOI":"10.1145\/309758.309780","volume":"27","author":"H Cass\u00e9","year":"1999","unstructured":"Cass\u00e9, H., F\u00e9raud, L., Rochange, C., Sainrat, P.: Using the abstract interpretation technique for static pointer analysis. SIGARCH Comput. Architect. News 27(1), 47\u201350 (1999)","journal-title":"SIGARCH Comput. Architect. News"},{"key":"24_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"334","DOI":"10.1007\/978-3-319-08867-9_22","volume-title":"Computer Aided Verification","author":"R Cavada","year":"2014","unstructured":"Cavada, R., et al.: The nuXmv symbolic model checker. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 334\u2013342. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-08867-9_22"},{"key":"24_CR23","doi-asserted-by":"publisher","unstructured":"Cavada, R., et al.: The NUXMV symbolic model checker. In: Biere, A., Bloem, R. (eds.) Computer Aided Verification - 26th International Conference, CAV 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 18-22, 2014. Proceedings. Lecture Notes in Computer Science, vol.\u00a08559, pp. 334\u2013342. Springer (2014). https:\/\/doi.org\/10.1007\/978-3-319-08867-9_22","DOI":"10.1007\/978-3-319-08867-9_22"},{"key":"24_CR24","unstructured":"Chen, D., Huang, R., Qu, B., Jiang, S.: Improving static analysis performance using rule-filtering technique. In: Reformat, M. (ed.) The 26th International Conference on Software Engineering and Knowledge Engineering, Hyatt Regency, Vancouver, BC, Canada, July 1-3, 2013, pp. 19\u201324. Knowledge Systems Institute Graduate School (2014)"},{"key":"24_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"85","DOI":"10.1007\/978-3-540-24622-0_9","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"E Clarke","year":"2004","unstructured":"Clarke, E., Kroening, D., Ouaknine, J., Strichman, O.: Completeness and complexity of bounded model checking. In: Steffen, B., Levi, G. (eds.) VMCAI 2004. LNCS, vol. 2937, pp. 85\u201396. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-24622-0_9"},{"key":"24_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"208","DOI":"10.1007\/978-3-540-39910-0_9","volume-title":"Verification: Theory and Practice","author":"E Clarke","year":"2003","unstructured":"Clarke, E., Veith, H.: Counterexamples revisited: principles, algorithms, applications. In: Dershowitz, N. (ed.) Verification: Theory and Practice. LNCS, vol. 2772, pp. 208\u2013224. Springer, Heidelberg (2003). https:\/\/doi.org\/10.1007\/978-3-540-39910-0_9"},{"key":"24_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"38","DOI":"10.1007\/978-3-319-96145-3_3","volume-title":"Computer Aided Verification","author":"B Cook","year":"2018","unstructured":"Cook, B.: Formal reasoning about the security of amazon web services. In: Chockler, H., Weissenbacher, G. (eds.) CAV 2018. LNCS, vol. 10981, pp. 38\u201347. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-96145-3_3"},{"issue":"1","key":"24_CR28","doi-asserted-by":"publisher","first-page":"34","DOI":"10.1007\/s10703-020-00344-2","volume":"57","author":"B Cook","year":"2021","unstructured":"Cook, B., Khazem, K., Kroening, D., Tasiran, S., Tautschnig, M., Tuttle, M.R.: Model checking boot code from AWS data centers. Formal Methods Syst. Des. 57(1), 34\u201352 (2021)","journal-title":"Formal Methods Syst. Des."},{"key":"24_CR29","doi-asserted-by":"crossref","unstructured":"Coppa, E., D\u2019Elia, D.C., Demetrescu, C.: Rethinking pointer reasoning in symbolic execution. In: Rosu, G., Penta, M.D., Nguyen, T.N. (eds.) Proceedings of the 32nd IEEE\/ACM International Conference on Automated Software Engineering, ASE 2017, Urbana, IL, USA, October 30 - November 03, 2017, pp. 613\u2013618. IEEE Computer Society (2017)","DOI":"10.1109\/ASE.2017.8115671"},{"key":"24_CR30","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: POPL, pp. 238\u2013252. ACM (1977)","DOI":"10.1145\/512950.512973"},{"key":"24_CR31","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Static determination of dynamic properties of generalized type unions. In: Language Design for Reliable Software, pp. 77\u201394. ACM (1977)","DOI":"10.1145\/800022.808314"},{"key":"24_CR32","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Systematic design of program analysis frameworks. In: POPL, pp. 269\u2013282. ACM Press (1979)","DOI":"10.1145\/567752.567778"},{"key":"24_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1007\/978-3-540-31987-0_3","volume-title":"Programming Languages and Systems","author":"P Cousot","year":"2005","unstructured":"Cousot, P., et al.: The ASTRE\u00c9 analyzer. In: Sagiv, M. (ed.) ESOP 2005. LNCS, vol. 3444, pp. 21\u201330. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/978-3-540-31987-0_3"},{"issue":"3","key":"24_CR34","doi-asserted-by":"publisher","first-page":"573","DOI":"10.1007\/s00165-014-0326-7","volume":"27","author":"F Kirchner","year":"2015","unstructured":"Kirchner, F., Kosmatov, N., Prevosto, V., Signoles, J., Yakobowski, B.: Frama-C: a software analysis perspective. Formal Aspects Comput. 27(3), 573\u2013609 (2015). https:\/\/doi.org\/10.1007\/s00165-014-0326-7","journal-title":"Formal Aspects Comput."},{"key":"24_CR35","doi-asserted-by":"crossref","unstructured":"D\u2019Abruzzo\u00a0Pereira, J., Vieira, M.: On the use of open-source C\/C++ static analysis tools in large projects. In: 2020 16th European Dependable Computing Conference (EDCC), pp. 97\u2013102 (2020)","DOI":"10.1109\/EDCC51268.2020.00025"},{"key":"24_CR36","doi-asserted-by":"crossref","unstructured":"Dijkstra, E.W.: Guarded commands, nondeterminacy and formal derivation of programs. Commun. ACM 18(8), 453-457 (1975)","DOI":"10.1145\/360933.360975"},{"key":"24_CR37","doi-asserted-by":"publisher","first-page":"340","DOI":"10.1007\/978-3-642-59412-0_19","volume-title":"Software Pioneers","author":"EW Dijkstra","year":"2002","unstructured":"Dijkstra, E.W.: EWD 1308: What Led to \u201cNotes on Structured Programming\u2019\u2019. In: Broy, M., Denert, E. (eds.) Software Pioneers, pp. 340\u2013346. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/978-3-642-59412-0_19"},{"key":"24_CR38","doi-asserted-by":"crossref","unstructured":"Dillig, I., Dillig, T., Aiken, A.: Automated error diagnosis using abductive inference. In: PLDI, pp. 181\u2013192. ACM (2012)","DOI":"10.1145\/2254064.2254087"},{"key":"24_CR39","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"351","DOI":"10.1007\/978-3-642-23702-7_26","volume-title":"Static Analysis","author":"AF Donaldson","year":"2011","unstructured":"Donaldson, A.F., Haller, L., Kroening, D., R\u00fcmmer, P.: Software verification using k-induction. In: Yahav, E. (ed.) SAS 2011. LNCS, vol. 6887, pp. 351\u2013368. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-23702-7_26"},{"key":"24_CR40","doi-asserted-by":"crossref","unstructured":"D\u2019Silva, V.V., Kroening, D., Weissenbacher, G.: A survey of automated techniques for formal software verification. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 27(7), 1165\u20131178 (2008)","DOI":"10.1109\/TCAD.2008.923410"},{"issue":"1\u20133","key":"24_CR41","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1016\/j.scico.2007.01.015","volume":"69","author":"MD Ernst","year":"2007","unstructured":"Ernst, M.D., et al.: The Daikon system for dynamic detection of likely invariants. Sci. Comput. Program. 69(1\u20133), 35\u201345 (2007)","journal-title":"Sci. Comput. Program."},{"key":"24_CR42","unstructured":"Ferdinand, C.: Worst case execution time prediction by static program analysis. In: IPDPS. IEEE Computer Society (2004)"},{"key":"24_CR43","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1007\/978-3-642-37036-6_8","volume-title":"Programming Languages and Systems","author":"JC Filli\u00e2tre","year":"2013","unstructured":"Filli\u00e2tre, J.C., Paskevich, A.: Why3 \u2014 where programs meet provers. In: Felleisen, M., Gardner, P. (eds.) ESOP 2013. LNCS, vol. 7792, pp. 125\u2013128. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-37036-6_8"},{"key":"24_CR44","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"500","DOI":"10.1007\/3-540-45251-6_29","volume-title":"FME 2001: Formal Methods for Increasing Software Productivity","author":"C Flanagan","year":"2001","unstructured":"Flanagan, C., Leino, K.R.M.: Houdini, an annotation assistant for ESC\/Java. In: Oliveira, J.N., Zave, P. (eds.) FME 2001. LNCS, vol. 2021, pp. 500\u2013517. Springer, Heidelberg (2001). https:\/\/doi.org\/10.1007\/3-540-45251-6_29"},{"key":"24_CR45","doi-asserted-by":"crossref","unstructured":"Flanagan, C., Leino, K.R.M., Lillibridge, M., Nelson, G., Saxe, J.B., Stata, R.: Extended static checking for java. In: PLDI, pp. 234\u2013245. ACM (2002)","DOI":"10.1145\/543552.512558"},{"key":"24_CR46","doi-asserted-by":"publisher","unstructured":"Floyd, R.W.: Assigning meanings to programs. In: Colburn, T.R., Fetzer, J.H., Rankin, T.L. (eds) Program Verification. Studies in Cognitive Systems, vol. 14. Springer, Dordrecht (1993). https:\/\/doi.org\/10.1007\/978-94-011-1793-7_4","DOI":"10.1007\/978-94-011-1793-7_4"},{"key":"24_CR47","unstructured":"Gibson-Robinson, T.: FDR3: the future of CSP model checking. In: Welch, P.H., Barnes, F.R.M., Broenink, J.F., Chalmers, K., Pedersen, J.B., Sampson, A.T. (eds.) 35th Communicating Process Architectures, CPA 2013, Edinburgh, Scotland, UK, August 25, 2013, pp. 321\u2013322. Open Channel Publishing Ltd. (2013)"},{"key":"24_CR48","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-02652-2_1","volume-title":"Model Checking Software","author":"P Godefroid","year":"2009","unstructured":"Godefroid, P.: Software model checking improving security of a billion computers. In: P\u0103s\u0103reanu, C.S. (ed.) SPIN 2009. LNCS, vol. 5578, pp. 1\u20131. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-02652-2_1"},{"key":"24_CR49","doi-asserted-by":"crossref","unstructured":"Gopinath, R., Jensen, C., Groce, A.: Code coverage for suite evaluation by developers. In: Jalote, P., Briand, L.C., van\u00a0der Hoek, A. (eds.) 36th International Conference on Software Engineering, ICSE \u201914, Hyderabad, India, May 31 - June 07, 2014, pp. 72\u201382. ACM (2014)","DOI":"10.1145\/2568225.2568278"},{"key":"24_CR50","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"152","DOI":"10.1007\/3-540-48234-2_11","volume-title":"Theoretical and Practical Aspects of SPIN Model Checking","author":"K Havelund","year":"1999","unstructured":"Havelund, K.: Java PathFinder a translator from Java to Promela. In: Dams, D., Gerth, R., Leue, S., Massink, M. (eds.) SPIN 1999. LNCS, vol. 1680, pp. 152\u2013152. Springer, Heidelberg (1999). https:\/\/doi.org\/10.1007\/3-540-48234-2_11"},{"key":"24_CR51","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"25","DOI":"10.1007\/11537328_4","volume-title":"Model Checking Software","author":"TA Henzinger","year":"2005","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R.: The BLAST software verification system. In: Godefroid, P. (ed.) SPIN 2005. LNCS, vol. 3639, pp. 25\u201326. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/11537328_4"},{"issue":"10","key":"24_CR52","doi-asserted-by":"publisher","first-page":"576","DOI":"10.1145\/363235.363259","volume":"12","author":"CAR Hoare","year":"1969","unstructured":"Hoare, C.A.R.: An axiomatic basis for computer programming. Commun. ACM 12(10), 576\u2013580 (1969)","journal-title":"Commun. ACM"},{"issue":"5","key":"24_CR53","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1109\/32.588521","volume":"23","author":"GJ Holzmann","year":"1997","unstructured":"Holzmann, G.J.: The model checker SPIN. IEEE Trans. Softw. Eng. 23(5), 279\u2013295 (1997)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"24_CR54","doi-asserted-by":"crossref","unstructured":"Jhala, R., Majumdar, R.: Software model checking. ACM Comput. Surv. 41(4), 21:1\u201321:54 (2009)","DOI":"10.1145\/1592434.1592438"},{"key":"24_CR55","unstructured":"Johnson, S.C.: Lint, a C program checker, pp. 78\u20131273 (1978)"},{"key":"24_CR56","doi-asserted-by":"publisher","unstructured":"K\u00e4stner, D., Wilhelm, R., Ferdinand, C.: Abstract interpretation in industry - experience and lessons learned. In: In: Hermenegildo, M.V., Morales, J.F. (eds) Static Analysis. SAS 2023. Lecture Notes in Computer Science, vol 14284. Springer, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-44245-2_2","DOI":"10.1007\/978-3-031-44245-2_2"},{"key":"24_CR57","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"451","DOI":"10.1007\/978-3-030-99527-0_30","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"M Kettl","year":"2022","unstructured":"Kettl, M., Lemberger, T.: The static analyzer infer in SV-COMP (competition contribution). In: TACAS 2022. LNCS, vol. 13244, pp. 451\u2013456. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-030-99527-0_30"},{"issue":"7","key":"24_CR58","doi-asserted-by":"publisher","first-page":"385","DOI":"10.1145\/360248.360252","volume":"19","author":"JC King","year":"1976","unstructured":"King, J.C.: Symbolic execution and program testing. Commun. ACM 19(7), 385\u2013394 (1976)","journal-title":"Commun. ACM"},{"key":"24_CR59","doi-asserted-by":"crossref","unstructured":"Klein, G., Elphinstone, K., et al.: seL4: formal verification of an OS kernel. In: SOSP, pp. 207\u2013220. ACM (2009)","DOI":"10.1145\/1629575.1629596"},{"key":"24_CR60","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"389","DOI":"10.1007\/978-3-642-54862-8_26","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"D Kroening","year":"2014","unstructured":"Kroening, D., Tautschnig, M.: CBMC \u2013 C bounded model checker. In: \u00c1brah\u00e1m, E., Havelund, K. (eds.) TACAS 2014. LNCS, vol. 8413, pp. 389\u2013391. Springer, Heidelberg (2014). https:\/\/doi.org\/10.1007\/978-3-642-54862-8_26"},{"key":"24_CR61","doi-asserted-by":"crossref","unstructured":"Kuznetsov, V., Kinder, J., Bucur, S., Candea, G.: Efficient state merging in symbolic execution. In: Vitek, J., Lin, H., Tip, F. (eds.) ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI \u201912, Beijing, China, June 11 - 16, 2012, pp. 193\u2013204. ACM (2012)","DOI":"10.1145\/2345156.2254088"},{"key":"24_CR62","doi-asserted-by":"crossref","unstructured":"Lahiri, S.K., Vaswani, K., Hoare, C.A.R.: Differential static analysis: opportunities, applications, and challenges. In: FoSER, pp. 201\u2013204. ACM (2010)","DOI":"10.1145\/1882362.1882405"},{"key":"24_CR63","doi-asserted-by":"crossref","unstructured":"Lattner, C., Adve, V.S.: LLVM: a compilation framework for lifelong program analysis and transformation. In: CGO, pp. 75\u201388. IEEE Computer Society (2004)","DOI":"10.1109\/CGO.2004.1281665"},{"key":"24_CR64","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"348","DOI":"10.1007\/978-3-642-17511-4_20","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"KRM Leino","year":"2010","unstructured":"Leino, K.R.M.: Dafny: an automatic program verifier for functional correctness. In: Clarke, E.M., Voronkov, A. (eds.) LPAR 2010. LNCS (LNAI), vol. 6355, pp. 348\u2013370. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-17511-4_20"},{"issue":"7","key":"24_CR65","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1145\/1538788.1538814","volume":"52","author":"X Leroy","year":"2009","unstructured":"Leroy, X.: Formal verification of a realistic compiler. Commun. ACM 52(7), 107\u2013115 (2009)","journal-title":"Commun. ACM"},{"key":"24_CR66","doi-asserted-by":"crossref","unstructured":"Logozzo, F.: Practical specification and verification with code contracts. In: HILT, pp.\u00a07\u20138. ACM (2013)","DOI":"10.1145\/2527269.2534188"},{"key":"24_CR67","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"299","DOI":"10.1007\/978-3-030-54994-7_22","volume-title":"Formal Methods. FM 2019 International Workshops","author":"Z Neha\u00ef","year":"2020","unstructured":"Neha\u00ef, Z., Bobot, F.: Deductive proof of industrial smart contracts using Why3. In: Sekerinski, E., et al. (eds.) FM 2019. LNCS, vol. 12232, pp. 299\u2013311. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-54994-7_22"},{"key":"24_CR68","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL","year":"2002","unstructured":"Nipkow, T., Wenzel, M., Paulson, L.C. (eds.): Isabelle\/HOL. LNCS, vol. 2283. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-45949-9"},{"key":"24_CR69","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"230","DOI":"10.1007\/978-3-642-04652-0_5","volume-title":"Advanced Functional Programming","author":"U Norell","year":"2009","unstructured":"Norell, U.: Dependently typed programming in Agda. In: Koopman, P., Plasmeijer, R., Swierstra, D. (eds.) AFP 2008. LNCS, vol. 5832, pp. 230\u2013266. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-04652-0_5"},{"key":"24_CR70","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"748","DOI":"10.1007\/3-540-55602-8_217","volume-title":"Automated Deduction\u2014CADE-11","author":"S Owre","year":"1992","unstructured":"Owre, S., Rushby, J.M., Shankar, N.: PVS: a prototype verification system. In: Kapur, D. (ed.) CADE 1992. LNCS, vol. 607, pp. 748\u2013752. Springer, Heidelberg (1992). https:\/\/doi.org\/10.1007\/3-540-55602-8_217"},{"key":"24_CR71","doi-asserted-by":"publisher","first-page":"275","DOI":"10.1016\/bs.adcom.2018.03.015","volume":"112","author":"M Papadakis","year":"2019","unstructured":"Papadakis, M., Kintis, M., Zhang, J., Jia, Y., Traon, Y.L., Harman, M.: Chapter six - mutation testing advances: an analysis and survey. Adv. Comput. 112, 275\u2013378 (2019)","journal-title":"Adv. Comput."},{"key":"24_CR72","doi-asserted-by":"crossref","unstructured":"Pasareanu, C.S., et al.: Combining unit-level symbolic execution and system-level concrete execution for testing NASA software. In: ISSTA, pp. 15\u201326. ACM (2008)","DOI":"10.1145\/1390630.1390635"},{"key":"24_CR73","doi-asserted-by":"publisher","first-page":"358","DOI":"10.1090\/S0002-9947-1953-0053041-6","volume":"74","author":"HG Rice","year":"1953","unstructured":"Rice, H.G.: Classes of recursively enumerable sets and their decision problems. Trans. Am. Math. Soc. 74, 358\u2013366 (1953)","journal-title":"Trans. Am. Math. Soc."},{"key":"24_CR74","doi-asserted-by":"crossref","unstructured":"Schmidt, D.A.: Data flow analysis is model checking of abstract interpretations. In: MacQueen, D.B., Cardelli, L. (eds.) POPL \u201998, Proceedings of the 25th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, San Diego, CA, USA, January 19\u201321, 1998, pp. 38\u201348. ACM (1998)","DOI":"10.1145\/268946.268950"},{"key":"24_CR75","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"62","DOI":"10.1007\/978-3-319-19458-5_5","volume-title":"Formal Methods for Industrial Critical Systems","author":"P Schrammel","year":"2015","unstructured":"Schrammel, P., Kroening, D., Brain, M., Martins, R., Teige, T., Bienm\u00fcller, T.: Successful use of incremental BMC in the automotive industry. In: N\u00fa\u00f1ez, M., G\u00fcdemann, M. (eds.) FMICS 2015. LNCS, vol. 9128, pp. 62\u201377. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-19458-5_5"},{"key":"24_CR76","doi-asserted-by":"crossref","unstructured":"Shen, H., Fang, J., Zhao, J.: EFindBugs: effective error ranking for findBugs. In: Fourth IEEE International Conference on Software Testing, Verification and Validation, ICST 2011, Berlin, Germany, March 21-25, 2011, pp. 299\u2013308. IEEE Computer Society (2011)","DOI":"10.1109\/ICST.2011.51"},{"key":"24_CR77","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"134","DOI":"10.1007\/978-3-540-79124-9_10","volume-title":"Tests and Proofs","author":"N Tillmann","year":"2008","unstructured":"Tillmann, N., de Halleux, J.: Pex\u2013white box test generation for .NET. In: Beckert, B., H\u00e4hnle, R. (eds.) TAP 2008. LNCS, vol. 4966, pp. 134\u2013153. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-79124-9_10"},{"key":"24_CR78","doi-asserted-by":"crossref","unstructured":"Turing, A.M.: On computable numbers, with an application to the entscheidungsproblem. Proc. London Math. Soc. s2-42(1), 230\u2013265 (1937)","DOI":"10.1112\/plms\/s2-42.1.230"},{"key":"24_CR79","doi-asserted-by":"crossref","unstructured":"Vernier-Mounier, I.: Symbolic executions of symmetrical parallel programs. In: 4th Euromicro Workshop on Parallel and Distributed Processing (PDP \u201996), January 24-26, 1996, Portugal, pp. 327\u2013335. IEEE Computer Society (1996)","DOI":"10.1109\/EMPDP.1996.500604"},{"key":"24_CR80","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1007\/978-3-030-41600-3_7","volume-title":"Verified Software. Theories, Tools, and Experiments","author":"Y Wang","year":"2020","unstructured":"Wang, Y., et al.: Formal verification of workflow policies for smart contracts in Azure Blockchain. In: Chakraborty, S., Navas, J.A. (eds.) VSTTE 2019. LNCS, vol. 12031, pp. 87\u2013106. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-41600-3_7"},{"key":"24_CR81","doi-asserted-by":"crossref","unstructured":"Wegman, M.N., Zadeck, F.K.: Constant propagation with conditional branches. In: Deusen, M.S.V., Galil, Z., Reid, B.K. (eds.) Conference Record of the Twelfth Annual ACM Symposium on Principles of Programming Languages, New Orleans, Louisiana, USA, January 1985, pp. 291\u2013299. ACM Press (1985)","DOI":"10.1145\/318593.318659"},{"issue":"2","key":"24_CR82","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/1050849.1050865","volume":"30","author":"B Xu","year":"2005","unstructured":"Xu, B., Qian, J., Zhang, X., Wu, Z., Chen, L.: A brief survey of program slicing. ACM SIGSOFT Softw. Eng. Notes 30(2), 1\u201336 (2005)","journal-title":"ACM SIGSOFT Softw. Eng. Notes"},{"key":"24_CR83","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"54","DOI":"10.1007\/3-540-48153-2_6","volume-title":"Correct Hardware Design and Verification Methods","author":"Y Yu","year":"1999","unstructured":"Yu, Y., Manolios, P., Lamport, L.: Model checking TLA+ specifications. In: Pierre, L., Kropf, T. (eds.) CHARME 1999. LNCS, vol. 1703, pp. 54\u201366. Springer, Heidelberg (1999). https:\/\/doi.org\/10.1007\/3-540-48153-2_6"}],"container-title":["Lecture Notes in Computer Science","Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-71177-0_24","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,11,28]],"date-time":"2024-11-28T01:11:00Z","timestamp":1732756260000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-71177-0_24"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,9,13]]},"ISBN":["9783031711763","9783031711770"],"references-count":83,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-71177-0_24","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2024,9,13]]},"assertion":[{"value":"13 September 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Formal Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Milan","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Italy","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"9 September 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"13 September 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"26","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"fm2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.fm24.polimi.it\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}