zbMATH — the first resource for mathematics

A decision procedure for bit-vectors and arrays. (English) Zbl 1135.68472
Damm, Werner (ed.) et al., Computer aided verification. 19th international conference, CAV 2007, Berlin, Germany, July 3–7, 2007. Proceedings. Berlin: Springer (ISBN 978-3-540-73367-6/pbk). Lecture Notes in Computer Science 4590, 519-531 (2007).
Summary: STP is a decision procedure for the satisfiability of quantifier-free formulas in the theory of bit-vectors and arrays that has been optimized for large problems encountered in software analysis applications. The basic architecture of the procedure consists of word-level pre-processing algorithms followed by translation to SAT. The primary bottlenecks in software verification and bug finding applications are large arrays and linear bit-vector arithmetic. New algorithms based on the abstraction-refinement paradigm are presented for reasoning about large arrays. A solver for bit-vector linear arithmetic is presented that eliminates variables and parts of variables to enable other transformations, and reduce the size of the problem that is eventually received by the SAT solver.
These and other algorithms have been implemented in STP, which has been heavily tested over thousands of examples obtained from several real-world applications. Experimental results indicate that the above mix of algorithms along with the overall architecture is far more effective, for a variety of applications, than a direct translation of the original formula to SAT or other comparable decision procedures.
For the entire collection see [Zbl 1119.68005].

68Q60 Specification and verification (program logics, model checking, etc.)
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
Full Text: DOI