Mihály Dobos-Kovács
ABSTRACT
The verification of safety-critical software systems is an algorithmically complex task, which often utilizes SMT (Satisfiability Modulo Theory) solvers for computing abstractions and refinements. It follows that the performance of SMT solvers impacts the performance of the abstraction-refinement-based verification process. Moreover, SMT solvers algorithmically affect the refinement process with either Craig interpolation or unsatisfiable cores. We evaluated eight versions of six different SMT solvers on software verification benchmarks to evaluate their effect on software model checking.
- Zsófia Ádám, Levente Bajczi, Mihály Dobos-Kovács, Ákos Hajdu, and Vince Molnár. 2022. Theta: portfolio of CEGAR-based analyses with dynamic algorithm selection (Competition Contribution). In Tools and Algorithms for the Construction and Analysis of Systems, Dana Fisman and Grigore Rosu (Eds.). Springer International Publishing, Cham, 474–478.Google Scholar
- Haniel Barbosa, Clark Barrett, Martin Brain, Gereon Kremer, Hanna Lachnitt, Makai Mann, Abdalrhman Mohamed, Mudathir Mohamed, Aina Niemetz, Andres Nötzli, Alex Ozdemir, Mathias Preiner, Andrew Reynolds, Ying Sheng, Cesare Tinelli, and Yoni Zohar. 2022. cvc5: A Versatile and Industrial-Strength SMT Solver. In Tools and Algorithms for the Construction and Analysis of Systems, Dana Fisman and Grigore Rosu (Eds.). Springer International Publishing, Cham, 415–442.Google Scholar
- Clark Barrett, Christopher L. Conway, Morgan Deters, Liana Hadarean, Dejan Jovanović, Tim King, Andrew Reynolds, and Cesare Tinelli. 2011. CVC4. In Computer Aided Verification, Ganesh Gopalakrishnanand Shaz Qadeer (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 171–177.Google Scholar
- Clark Barrett, Aaron Stump, Cesare Tinelli, 2010. The smt-lib standard: Version 2.0. In Proceedings of the 8th international workshop on satisfiability modulo theories (Edinburgh, England), Vol. 13. 14.Google Scholar
- Clark Barrett and Cesare Tinelli. 2018. Satisfiability Modulo Theories. Springer International Publishing, Cham, 305–343. https://doi.org/10.1007/978-3-319-10575-8_11Google ScholarCross Ref
- Dirk Beyer. 2012. Competition on Software Verification. In Tools and Algorithms for the Construction and Analysis of Systems, Cormac Flanaganand Barbara König (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 504–524.Google Scholar
- Dirk Beyer, Thomas A. Henzinger, and Grégory Théoduloz. 2007. Configurable Software Verification: Concretizing the Convergence of Model Checking and Program Analysis. In Computer Aided Verification, Werner Damm and Holger Hermanns (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 504–518.Google Scholar
- Dirk Beyer and Stefan Löwe. 2013. Explicit-State Software Model Checking Based on CEGAR and Interpolation. In Fundamental Approaches to Software Engineering, Vittorio Cortellessa and Dániel Varró (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 146–162.Google Scholar
- Angelo Brillout, Daniel Kroening, Philipp Rümmer, and Thomas Wahl. 2011. An Interpolating Sequent Calculus for Quantifier-Free Presburger Arithmetic. Journal of Automated Reasoning 47 (2011), 341–367. Issue 4. http://dx.doi.org/10.1007/s10817-011-9237-yGoogle ScholarDigital Library
- Roberto Bruttomesso, Alessandro Cimatti, Anders Franzén, Alberto Griggio, and Roberto Sebastiani. 2008. The MathSAT 4 SMT Solver. In Computer Aided Verification, Aarti Gupta and Sharad Malik (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 299–303.Google Scholar
- Jürgen Christ, Jochen Hoenicke, and Alexander Nutz. 2012. SMTInterpol: An Interpolating SMT Solver. In Model Checking Software, Alastair Donaldson and David Parker (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 248–254.Google Scholar
- Edmund Clarke, Orna Grumberg, Somesh Jha, Yuan Lu, and Helmut Veith. 2000. Counterexample-Guided Abstraction Refinement. In Computer Aided Verification, E. Allen Emerson and Aravinda Prasad Sistla (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 154–169.Google ScholarCross Ref
- Edmund M. Clarke, Thomas A. Henzinger, and Helmut Veith. 2018. Introduction to Model Checking. In Handbook of Model Checking, Edmund M. Clarke, Thomas A. Henzinger, Helmut Veith, and Roderick Bloem (Eds.). Springer International Publishing, Cham, 1–26. https://doi.org/10.1007/978-3-319-10575-8_1Google ScholarCross Ref
- Leonardo de Moura and Nikolaj Bjørner. 2008. Z3: An Efficient SMT Solver. In Tools and Algorithms for the Construction and Analysis of Systems, C. R. Ramakrishnanand Jakob Rehof (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 337–340.Google Scholar
- Daniel Dietsch, Matthias Heizmann, Betim Musa, Alexander Nutz, and Andreas Podelski. 2017. Craig vs. Newton in Software Model Checking. In Proceedings of the 2017 11th Joint Meeting on Foundations of Software Engineering (Paderborn, Germany) (ESEC/FSE 2017). Association for Computing Machinery, New York, NY, USA, 487–497. https://doi.org/10.1145/3106237.3106307Google ScholarDigital Library
- Mihály Dobos-Kovács, Ákos Hajdu, and András Vörös. 2021. Bitvector Support in the Theta Formal Verification Framework. In 2021 10th Latin-American Symposium on Dependable Computing (LADC). IEEE, 01–08. https://doi.org/10.1109/LADC53747.2021.9672595Google ScholarCross Ref
- Ákos Hajdu and Zoltán Micskei. 2020. Efficient Strategies for CEGAR-based Model Checking. Journal of Automated Reasoning 64, 6 (2020), 1051–1091. https://doi.org/10.1007/s10817-019-09535-xGoogle ScholarDigital Library
- Ranjit Jhala, Andreas Podelski, and Andrey Rybalchenko. 2018. Predicate Abstraction for Program Verification. Springer International Publishing, Cham, 447–491. https://doi.org/10.1007/978-3-319-10575-8_15Google ScholarCross Ref
- Nikita Malyshev, Irina Dudina, Daniil Kutz, Alexander Novikov, and Sergey Vartanov. 2019. SMT Solvers in Application to Static and Dynamic Symbolic Execution: A Case Study. In 2019 Ivannikov Ispras Open Conference (ISPRAS). IEEE, 9–15.Google ScholarCross Ref
- Kenneth L. McMillan. 2005. Applications of Craig Interpolants in Model Checking. In Tools and Algorithms for the Construction and Analysis of Systems. Springer Berlin Heidelberg, Berlin, Heidelberg, 1–12.Google Scholar
- Sabino Francesco Roselli, Kristofer Bengtsson, and Knut Åkesson. 2018. SMT solvers for job-shop scheduling problems: Models comparison and performance evaluation. In 2018 IEEE 14th International Conference on Automation Science and Engineering (CASE). IEEE, 547–552.Google ScholarDigital Library
- Tamás Tóth, Ákos Hajdu, András Vörös, Zoltán Micskei, and István Majzik. 2017. Theta: a Framework for Abstraction Refinement-Based Model Checking. In Proceedings of the 17th Conference on Formal Methods in Computer-Aided Design, Daryl Stewart and Georg Weissenbacher (Eds.). IEEE, 176–179. https://doi.org/10.23919/FMCAD.2017.8102257Google ScholarCross Ref
- Tjark Weber, Sylvain Conchon, David Déharbe, Matthias Heizmann, Aina Niemetz, and Giles Reger. 2019. The SMT competition 2015–2018. Journal on Satisfiability, Boolean Modeling and Computation 11, 1(2019), 221–259.Google ScholarCross Ref
Index Terms
- Evaluation of SMT solvers in abstraction-based software model checking
Recommendations
Regular model checking for LTL(MSO)
Regular model checking is a form of symbolic model checking for parameterized and infinite-state systems whose states can be represented as words of arbitrary length over a finite alphabet, in which regular sets of words are used to represent sets of ...
Bounded model checking of software using SMT solvers instead of SAT solvers
SPIN'06: Proceedings of the 13th international conference on Model Checking SoftwareC Bounded Model Checking (CBMC) has proven to be a successful approach to automatic software analysis. The key idea is to (i) build a propositional formula whose models correspond to program traces (of bounded length) that violate some given property ...
Infinite-state invariant checking with IC3 and predicate abstraction
We address the problem of verifying invariant properties on infinite-state systems. We present a novel approach, IC3ia, for generalizing the IC3 invariant checking algorithm from finite-state to infinite-state transition systems, expressed over some ...
Comments