×

Deciding separation logic formulae by SAT and incremental negative cycle elimination. (English) Zbl 1143.68583

Sutcliffe, Geoff (ed.) et al., Logic for programming, artificial intelligence, and reasoning. 12th international conference, LPAR 2005, Montego Bay, Jamaica, December 2–6, 2005. Proceedings. Berlin: Springer (ISBN 978-3-540-30553-8/pbk). Lecture Notes in Computer Science 3835, 322-336 (2005).
Summary: Separation logic is a subset of the quantifier-free first-order logic. It has been successfully used in the automated verification of systems that have large (or unbounded) integer-valued state variables, such as pipelined processor designs and timed systems. In this paper, we present a fast decision procedure for separation logic, which combines Boolean satisfiability (SAT) with a graph-based incremental negative cycle elimination algorithm. Our solver abstracts a separation logic formula into a Boolean formula by replacing each predicate with a Boolean variable. Transitivity constraints over predicates are detected from the constraint graph and added on a need-to basis. Our solver handles Boolean and theory conflicts uniformly at the Boolean level. The graph-based algorithm supports not only incremental theory propagation, but also constant time theory backtracking without using a cumbersome history stack. Experimental results on a large set of benchmarks show that our new decision procedure is scalable, and outperforms existing techniques for this logic.
For the entire collection see [Zbl 1134.68011].

MSC:

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

Software:

Chaff; BerkMin
PDFBibTeX XMLCite
Full Text: DOI