×

Abstraction-based satisfiability solving of Presburger arithmetic. (English) Zbl 1103.68626

Alur, Rajeev (ed.) et al., Computer aided verification. 16th international conference, CAV 2004, Boston, MA, USA, July 13–17, 2004. Proceedings. Berlin: Springer (ISBN 3-540-22342-8/pbk). Lecture Notes in Computer Science 3114, 308-320 (2004).
Summary: We present a new abstraction-based framework for deciding satisfiability of quantifier-free Presburger arithmetic formulas. Given a Presburger formula \(\phi\), our algorithm invokes a SAT solver to produce proofs of unsatisfiability of approximations of \(\phi\). These proofs are in turn used to generate abstractions of \(\phi\) as inputs to a theorem prover. The SAT-encodings of the approximations of \(\phi\) are obtained by instantiating the variables of the formula over finite domains. The satisfying integer assignments provided by the theorem prover are then used to selectively increase domain sizes and generate fresh SAT-encodings of \(\phi\). The efficiency of this approach derives from the ability of SAT solvers to extract small unsatisfiable cores, leading to small abstracted formulas. We present experimental results which suggest that our algorithm is considerably more efficient than directly invoking the theorem prover on the original formula.
For the entire collection see [Zbl 1056.68003].

MSC:

68Q60 Specification and verification (program logics, model checking, etc.)
03B35 Mechanization of proofs and logical operations
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)

Software:

TLA; OPBDP
PDFBibTeX XMLCite
Full Text: DOI