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; Yices; HMC; Princess; Mjollnir; Boogie; nuXmv; MiniSat; SeaHorn; Datalog; TPTP; c2i; Ivy; Eldarica; UFO; FLATA; CVC4; SIMPLIFY; SMT-LIB; nncontroller Cited in: 18 Publications all top 5 Cited by 58 Authors 3 Kobayashi, Naoki 3 Kuncak, Viktor 2 Gurfinkel, Arie 2 Reynolds, Andrew 2 Sato, Ryosuke 2 Unno, Hiroshi 1 Barrett, Clark W. 1 Bjørner, Nikolaj S. 1 Bodik, Rastislav 1 Bromberger, Martin 1 Chaki, Sagar 1 Chakraborty, Supratik 1 Champion, Adrien 1 Chiba, Tomoya 1 Cimatti, Alessandro 1 D’Antoni, Loris 1 De Angelis, Emanuele 1 Deters, Morgan 1 Dragoste, Irina 1 Dutertre, Bruno 1 Faqeh, Rasha 1 Fedyukovich, Grigory 1 Feldman, Yotam M. Y. 1 Fetzer, Christof 1 Fioravanti, Fabio 1 Frumkin, Asya 1 Griggio, Alberto 1 Hojjat, Hossein 1 Hu, Qinheping 1 Irfan, Ahmed 1 John, Ajith K. 1 Jovanović, Dejan 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 McMillan, Kenneth L. 1 Mordvinov, Dmitriĭ Aleksandrovich 1 Padon, Oded 1 Pettorossi, Alberto 1 Proietti, Maurizio 1 Reps, Thomas W. 1 Roveri, Marco 1 Rümmer, Philipp 1 Rybalchenko, Andrey 1 Sagiv, Mooly 1 Sakayori, Ken 1 Sato, Issei 1 Sebastiani, Roberto 1 Sekiyama, Taro 1 Shimoda, Takumi 1 Shoham, Sharon 1 Terauchi, Tachio 1 Tinelli, Cesare 1 Weidenbach, Christoph Cited in 4 Serials 6 Formal Methods in System Design 1 Journal of Automated Reasoning 1 Theory and Practice of Logic Programming 1 Modelirovanie i Analiz Informatsionnykh Sistem Cited in 3 Fields 18 Computer science (68-XX) 5 Mathematical logic and foundations (03-XX) 1 Numerical analysis (65-XX) Citations by Year