×

Spacer

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; CVC4; SeaHorn; Yices; SMT-LIB; MoCHi; Boogie; GitHub; Princess; RAHFT; HMC; VeriMAP; MathSAT5; VAMPIRE; Eldarica; FLATA; c2i; SMTInterpol; SIMPLIFY; UFO
Cited in: 30 Documents
all top 5

Cited by 79 Authors

7 Kobayashi, Naoki
4 Sato, Ryosuke
3 De Angelis, Emanuele
3 Fioravanti, Fabio
3 Gurfinkel, Arie
3 Kuncak, Viktor
3 Pettorossi, Alberto
3 Proietti, Maurizio
2 Barrett, Clark W.
2 Fedyukovich, Grigory
2 Griggio, Alberto
2 Irfan, Ahmed
2 McMillan, Kenneth L.
2 Padon, Oded
2 Reynolds, Andrew
2 Sakayori, Ken
2 Tsukada, Takeshi
2 Unno, Hiroshi
1 Asada, Kazuyuki
1 Bjørner, Nikolaj S.
1 Bodik, Rastislav
1 Bouajjani, Ahmed
1 Boutglay, Wael-Amine
1 Bromberger, Martin
1 Chaki, Sagar
1 Chakraborty, Supratik
1 Champion, Adrien
1 Chernigovskaia, Lidiia
1 Chiba, Tomoya
1 Cimatti, Alessandro
1 D’Antoni, Loris
1 Deters, Morgan
1 Dragoste, Irina
1 Dutertre, Bruno
1 Faqeh, Rasha
1 Feldman, Yotam M. Y.
1 Fetzer, Christof
1 Frumkin, Asya
1 Gallagher, John P.
1 García-Contreras, Isabel
1 Habermehl, Peter
1 Hermenegildo, Manuel V.
1 Hojjat, Hossein
1 Hu, Qinheping
1 Ishikawa, Takuma
1 Itzhaky, Shachar
1 John, Ajith K.
1 Jovanović, Dejan
1 Katsura, Hiroyuki
1 Kaufman, Samuel J.
1 Kim, Jinwoo
1 King, Tim
1 Komuravelli, Anvesh
1 Koskinen, Eric
1 Krötzsch, Markus
1 Lhoták, Ondřej
1 Mann, Makai
1 Matsushita, Yusuke
1 Mordvinov, Dmitriĭ Aleksandrovich
1 Mukai, Ryoya
1 Navas, Jorge A.
1 Peled, Matan I.
1 Reps, Thomas W.
1 Rothenberg, Bat-Chen
1 Roveri, Marco
1 Rümmer, Philipp
1 Rybalchenko, Andrey
1 Sagiv, Mooly
1 Sato, Issei
1 Sebastiani, Roberto
1 Sekiyama, Taro
1 Shimoda, Takumi
1 Shoham, Sharon
1 Shoshi, Tsubasa
1 Terauchi, Tachio
1 Tinelli, Cesare
1 Vick, Cole
1 Weidenbach, Christoph
1 Zavalía, Lucas

Citations by Year