swMATH ID: 19496
Software Authors: Komuravelli, Anvesh; Gurfinkel, Arie; Chaki, Sagar
Description: 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.
Homepage: http://link.springer.com/article/10.1007%2Fs10703-016-0249-4
Keywords: model checking; may-must; satisfiability; quantifier elimination; recursion; compositional
Related Software: z3; Yices; HMC; Princess; Mjollnir; Boogie; nuXmv; MiniSat; SeaHorn; Datalog; TPTP; c2i; Ivy; Eldarica; UFO; FLATA; CVC4; SIMPLIFY; SMT-LIB; nncontroller
Cited in: 18 Publications

Citations by Year