CMU-CS-02-132
Computer Science Department
School of Computer Science, Carnegie Mellon University



CMU-CS-02-132

Reducing Separation Formulas to Propositional Logic

Ofer Strichman, Sanjit A. Seshia, Randal E. Bryant

April 2002

CMU-CS-02-132.ps
CMU-CS-02-132.pdf

A short version of this report titled, Deciding Separation Formulas with SAT
appeared in the Proceedings of the 14th International Conference on
Computer Aided Verification
, Copenhagen, Denmark, July 2002.

Keywords: Verification, decision-procedure, separation logic, difference logic, SAT


We show a reduction to propositional logic from a Boolean combination of inequalities of the form x >= y + c and x > y + c, where c is a constant and x,y are variables of type real or integer. Equalities and uninterpreted functions can be expressed in this logic as well. We discuss the advantages of using this reduction as compared to competing methods, and present experimental results that support our claims.

21 pages


Return to: SCS Technical Report Collection
School of Computer Science homepage

This page maintained by reports@cs.cmu.edu