Bounded model checking of software using SMT solvers instead of SAT solvers. (English) Zbl 1178.68148

Valmari, Antti (ed.), Model checking software. 13th international SPIN workshop, Vienna, Austria, March 30 – April 1, 2006. Proceedings. Berlin: Springer (ISBN 3-540-33102-6/pbk). Lecture Notes in Computer Science 3925, 146-162 (2006).
Summary: C 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 and (ii) use state-of-the-art SAT solvers to check the resulting formulae for satisfiability. In this paper we propose a generalisation of the CBMC approach based on an encoding into richer (but still decidable) theories than propositional logic. We show that our approach may lead to considerably more compact formulae than those obtained with CBMC. We have built a prototype implementation of our technique that uses a Satisfiability Modulo Theories (SMT) solver to solve the resulting formulae. Computer experiments indicate that our approach compares favourably with and on some significant problems outperforms CBMC.
For the entire collection see [Zbl 1103.68011].


68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
68Q60 Specification and verification (program logics, model checking, etc.)
Full Text: DOI