This article provides an innovative approach for verification by model checking of programs that undergo continuous changes. To tackle the problem of repeating the entire model checking for each new version of the program, our approach verifies programs incrementally. It reuses computational history of the previous program version, namely function summaries. In particular, the summaries are over-approximations of the bounded program behaviors. Whenever reusing of summaries is not possible straight away, our algorithm repairs the summaries to maximize the chance of reusability of them for subsequent runs. We base our approach on satisfiability modulo theories (SMT) to take full advantage of lightweight modeling approach and at the same time the ability to provide concise function summarization. Our approach leverages pre-computed function summaries in SMT to localize the checks of changed functions. Furthermore, to exploit the trade-off between precision and performance, our approach relies on the use of an SMT solver, not only for underlying reasoning, but also for program modeling and the adjustment of its precision. On the benchmark suite of primarily Linux device drivers versions, we demonstrate that our algorithm achieves an order of magnitude speedup compared to prior approaches.

Charles University Prague Czech Republic

Florida State University Tallahassee FL USA

Università della Svizzera italiana Lugano Switzerland

See more in PubMed

Clarke EM, Emerson EA (1981) Design and synthesis of synchronization skeletons using branching-time temporal logic. In: Workshop on logics of programs, pp 52–71. Springer, Heidelberg

Queille J, Sifakis J (1982) Specification and verification of concurrent systems in CESAR. In: 5th International symposium on programming, pp 337–351

Biere A, Cimatti A, Clarke EM, Zhu Y (1999) Symbolic model checking without BDDs. In: TACAS 1999, vol 1579, pp 193–207. Springer, Heidelberg

Fedyukovich G, Sery O, Sharygina N (2013) eVolCheck: Incremental upgrade checker for C. In: TACAS 2013, vol 7795, pp 292–307. Springer, Heidelberg

Barrett C, Sebastiani R, Seshia S, Tinelli C (2009) Satisfiability modulo theories, vol 185, 1st edn., pp 825–885

de Moura LM, Bjørner N (2009) Satisfiability modulo theories: An appetizer. In: SBMF 2009. LNCS, vol 5902, pp 23–36. Springer, Heidelberg

Craig W. Three uses of the herbrand–Gentzen theorem in relating model theory and proof theory. J Symb Log. 1957;22(3):269–285. doi: 10.2307/2963594. DOI

Sery O, Fedyukovich G, Sharygina N (2011) Interpolation-based function summaries in bounded model checking. In: HVC 2011, vol 7261, pp 160–175. Springer, Heidelberg

Asadi S, Blicha M, Fedyukovich G, Hyvärinen AEJ, Even-Mendoza K, Sharygina N, Chockler H (2018) Function summarization modulo theories. In: LPAR-22, vol 57, pp 56–75. EasyChair, England & Wales

Rollini SF, Alt L, Fedyukovich G, Hyvärinen A, Sharygina N (2013) PeRIPLO: A framework for producing effective interpolants in SAT-based software verification. In: LPAR 2013, vol 8312, pp 683–693. Springer, Heidelberg

Alt L, Asadi S, Chockler H, Even-Mendoza K, Fedyukovich G, Hyvärinen A, Sharygina N (2017) HiFrog: SMT-based function summarization for software verification. In: TACAS 2017, vol 10206, pp 207–213. Springer, Heidelberg

Sery O, Fedyukovich G, Sharygina N (2012) Incremental upgrade checking by means of interpolation-based function summaries. In: FMCAD 2012, pp 114–121. IEEE, New York

Fedyukovich G, Sery O, Sharygina N. Flexible SAT-based framework for incremental bounded upgrade checking. STTT. 2017;19(5):517–534. doi: 10.1007/s10009-015-0405-y. DOI

Asadi S, Blicha M, Hyvärinen A, Fedyukovich G, Sharygina N (2020) Incremental verification by SMT-based summary repair. In: FMCAD 2020. IEEE, New York

Silva T, Porto C, da S Alves EH, Cordeiro LC, Rocha H (2021) Verifying security vulnerabilities in large software systems using multi-core k-induction. CoRR arXiv:abs/2102.02368

Kroening D, Tautschnig M (1976) CBMC—C bounded model checker. In: TACAS 2014, vol 42, pp 389–391. Springer, Heidelberg

Clarke E, Kroening D, Lerda F (2004) A tool for checking ANSI-C programs. In: TACAS 2004, vol 2988, pp 168–176. Springer, Berlin, Heidelberg

McMillan KL (2003) Interpolation and SAT-based model checking. In: CAV 2003, pp 1–13

Henzinger T, Jhala R, Majumdar R, McMillan KL (2004) Abstractions from Proofs. In: POPL

Asadi S, Blicha M, Hyvärinen A, Fedyukovich G, Sharygina N (2020) Farkas-based tree interpolation. In: SAS 2020. Springer, Heidelberg

Blanc R, Gupta A, Kovács L, Kragl B (2013) Tree interpolation in Vampire. In: LPAR 2013, vol 8312, pp 173–181. Springer, Berlin

Komuravelli A, Gurfinkel A, Chaki S, Clarke EM (2013) Automatic abstraction in SMT-based unbounded software model checking. In: CAV 2013. LNCS, vol 8044, pp 846–862. Springer, Berlin

Fedyukovich G, Bodík R (2018) Accelerating Syntax-Guided Invariant Synthesis. In: TACAS, 2018, vol 10805, pp 251–269. Springer, Heidelberg

Flanagan C, Leino KRM (2001) Houdini, an annotation assistant for esc/java. In: FME 2001, vol 2021, pp 500–517. Springer, Heidelberg

Schrijver A. Theory of linear and integer programming. Wiley-Interscience series in discrete mathematics and optimization. London: Wiley, Sons; 1999.

McMillan KL. An interpolating theorem prover. Theor Comput Sci. 2005;345(1):101–121. doi: 10.1016/j.tcs.2005.07.003. DOI

Blicha M, Hyvärinen A, Kofron J, Sharygina N (2019) Decomposing Farkas interpolants. In: TACAS 2019, vol 11427, pp 3–20. Springer, Heidelberg

Alt L, Hyvärinen A, Asadi S, Sharygina N (2017) Duality-based interpolation for quantifier-free equalities and uninterpreted functions. In: FMCAD 2017, pp 39–46. FMCAD Inc, Austin, Texas

Pudlák P. Lower bounds for resolution and cutting plane proofs and monotone computations. J Symb Log. 1997;62(3):981–998. doi: 10.2307/2275583. DOI

Christ J, Hoenicke J. Proof tree preserving tree interpolation. J Autom Reasoning. 2016;57(1):67–95. doi: 10.1007/s10817-016-9365-5. DOI

Gurfinkel A, Rollini SF, Sharygina N (2013) Interpolation properties and SAT-based model checking. In: ATVA 2013, pp 255–271

Hyvärinen A, Marescotti M, Alt L, Sharygina N (2016) OpenSMT2: An SMT solver for multi-core and cloud computing. In: SAT 2016, vol 9710, pp 547–553. Springer, Heidelberg

Alt L, Fedyukovich G, Hyvärinen A, Sharygina N (2016) A proof-sensitive approach for small propositional interpolants. In: VSTTE 2015, vol 9593, pp 1–18. Springer, Berlin, Heidelberg

Beyer D, Löwe S, Novikov E, Stahlbauer A, Wendler P (2013) Precision reuse for efficient regression verification. In: ESEC/FSE 2013, pp 389–399. ACM, New York

Conway CL, Namjoshi KS, Dams D, Edwards SA (2005) Incremental algorithms for inter-procedural analysis of safety properties. In: CAV 2005, vol 3576, pp 449–461. Springer, Heidelberg

Trostanetski A, Grumberg O, Kroening D (2017) Modular demand-driven analysis of semantic difference for program versions. In: SAS 2017, vol 10422, pp 405–427. Springer, Cham

He F, Yu Q, Cai L (2018) When regression verification meets CEGAR. CoRR arXiv:abs/1806.04829

Rothenberg B, Dietsch D, Heizmann M (2018) Incremental verification using trace abstraction. In: Static analysis—25th international symposium, SAS 2018, pp 364–382

Beyer D, Jakobs M, Lemberger T (2020) Difference verification with conditions. In: SEFM 2020, vol 12310, pp 133–154. Springer, Cham

Lauterburg S, Sobeih A, Marinov D, Viswanathan M (2008) Incremental state-space exploration for programs with dynamically allocated data. In: ICSE 2008, pp 291–300. ACM, New York

Visser W, Geldenhuys J, Dwyer MB (2012) Green: reducing, reusing and recycling constraints in program analysis. In: SIGSOFT/FSE 2012, p 58. ACM, New York

Fedyukovich G, Gurfinkel A, Sharygina N (2014) Incremental verification of compiler optimizations. In: NFM 2014, pp 300–306

Fedyukovich G, Gurfinkel A, Sharygina N (2016) Property directed equivalence via abstract simulation. In: Proc. CAV 2016, vol 9780, Part II, pp 433–453. Springer, Cham

Hardin RH, Kurshan RP, McMillan KL, Reeds JA, Sloane NJA (1996) Efficient regression verification. In: Proc. WODES’96, pp 147–150. IEEE, Proc

Godlin B, Strichman O (2009) Regression verification. In: The 46th design automation conference, DAC, pp 466–471. ACM, New York

Lahiri SK, McMillan KL, Sharma R, Hawblitzel C (2013) Differential assertion checking. In: ESEC/FSE 2013, pp 345–355. ACM, New York

Pick L, Fedyukovich G, Gupta A (2018) Exploiting synchrony and symmetry in relational verification. In: CAV 2018, Part I, vol 10981, pp 164–182. Springer, Cham

Shemer R, Gurfinkel A, Shoham S, Vizel Y (2019) Property directed self composition. In: CAV 2019, vol 11561, pp 161–179. Springer, Heidelberg

Mordvinov D, Fedyukovich G (2019) Property directed inference of relational invariants. In: FMCAD 2019, pp 152–160. IEEE, San Jose

Felsing D, Grebing S, Klebanov V, Rümmer P, Ulbrich M (2014) Automating regression verification. In: ASE 2014, pp 349–360. ACM, New York

Yang G, Khurshid S, Person S, Rungta N (2014) Property differencing for incremental checking. In: ICSE 2014, pp 1059–1070. ACM, New York

Lahiri SK, Hawblitzel C, Kawaguchi M, Rebêlo H (2012) SYMDIFF: A language-agnostic semantic diff tool for imperative programs. In: CAV 2012, vol 7358, pp 712–717. Springer, Heidelberg

Godefroid P, Lahiri SK, Rubio-González C (2011) Statically validating must summaries for incremental compositional dynamic test generation. In: SAS 2011, vol 6887, pp 112–128. Springer, Heidelberg

McMillan KL (2010) Lazy annotation for program testing and verification. In: CAV 2010. LNCS, vol 6174, pp 104–118. Springer, Heidelberg (2010)

Albarghouthi A, Gurfinkel A, Chechik M (2012) Whale: An interpolation-based algorithm for inter-procedural verification. In: VMCAI 2012. LNCS, vol 7148, pp 39–55. Springer, Heidelberg (2012)