Sciweavers

Share
LPAR
2005
Springer

Deciding Separation Logic Formulae by SAT and Incremental Negative Cycle Elimination

11 years 5 months ago
Deciding Separation Logic Formulae by SAT and Incremental Negative Cycle Elimination
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 cremental 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 proc...
Chao Wang, Franjo Ivancic, Malay K. Ganai, Aarti G
Added 28 Jun 2010
Updated 28 Jun 2010
Type Conference
Year 2005
Where LPAR
Authors Chao Wang, Franjo Ivancic, Malay K. Ganai, Aarti Gupta
Comments (0)
books