Spacer

SMT-based model checking for recursive programs. We present an SMT-based symbolic model checking algorithm for safety verification of recursive programs. The algorithm is modular and analyzes procedures individually. Unlike other SMT-based approaches, it maintains both over- and under-approximations of procedure summaries. Under-approximations are used to analyze procedure calls without inlining. Over-approximations are used to block infeasible counterexamples and detect convergence to a proof. We show that for programs and properties over a decidable theory, the algorithm is guaranteed to find a counterexample, if one exists. However, efficiency depends on an oracle for quantifier elimination (QE). For Boolean programs, the algorithm is a polynomial decision procedure, matching the worst-case bounds of the best BDD-based algorithms. For Linear Arithmetic (integers and rationals), we give an efficient instantiation of the algorithm by applying QE lazily. We use existing interpolation techniques to over-approximate QE and introduce Model Based Projection to under-approximate QE. Empirical evaluation on SV-COMP benchmarks shows that our algorithm improves significantly on the state-of-the-art.


References in zbMATH (referenced in 11 articles )

Showing results 1 to 11 of 11.
Sorted by year (citations)

  1. Champion, Adrien; Chiba, Tomoya; Kobayashi, Naoki; Sato, Ryosuke: ICE-based refinement type discovery for higher-order functional programs (2020)
  2. Fedyukovich, Grigory; Kaufman, Samuel J.; Bodík, Rastislav: Learning inductive invariants by sampling from frequency distributions (2020)
  3. Reynolds, Andrew; Kuncak, Viktor; Tinelli, Cesare; Barrett, Clark; Deters, Morgan: Refutation-based synthesis in SMT (2019)
  4. Cimatti, Alessandro; Griggio, Alberto; Irfan, Ahmed; Roveri, Marco; Sebastiani, Roberto: Invariant checking of NRA transition systems via incremental reduction to LRA with EUF (2017)
  5. Frumkin, Asya; Feldman, Yotam M. Y.; Lhoták, Ondřej; Padon, Oded; Sagiv, Mooly; Shoham, Sharon: Property directed reachability for proving absence of concurrent modification errors (2017)
  6. Reynolds, Andrew; King, Tim; Kuncak, Viktor: Solving quantified linear arithmetic by counterexample-guided instantiation (2017)
  7. John, Ajith K.; Chakraborty, Supratik: A layered algorithm for quantifier elimination from linear modular constraints (2016)
  8. Komuravelli, Anvesh; Gurfinkel, Arie; Chaki, Sagar: SMT-based model checking for recursive programs (2016)
  9. Bjørner, Nikolaj; Gurfinkel, Arie; McMillan, Ken; Rybalchenko, Andrey: Horn clause solvers for program verification (2015)
  10. Rümmer, Philipp; Hojjat, Hossein; Kuncak, Viktor: On recursion-free Horn clauses and Craig interpolation (2015)
  11. Komuravelli, Anvesh; Gurfinkel, Arie; Chaki, Sagar: SMT-based model checking for recursive programs (2014) ioport