Deciding separation logic formulae by SAT and incremental negative cycle elimination

Chao Wang, Franjo Ivančić, Malay Ganai, Aarti Gupta

Research output: Contribution to journalConference article

16 Scopus citations

Abstract

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.

Original languageEnglish (US)
Pages (from-to)322-336
Number of pages15
JournalLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume3835 LNAI
DOIs
StatePublished - 2005
Externally publishedYes
Event12th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, LPAR 2005 - Montego Bay, Jamaica
Duration: Dec 2 2005Dec 6 2005

All Science Journal Classification (ASJC) codes

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Deciding separation logic formulae by SAT and incremental negative cycle elimination'. Together they form a unique fingerprint.

  • Cite this