A hybrid SAT-based decision procedure for separation logic with uninterpreted functions

SAT-based decision procedures for quantifier-free fragments of firstorder logic have proved to be useful in formal verification. These decision procedures are either based on encoding atomic subformulas with Boolean variables, or by encoding integer variables as bit-vectors. Based on evaluating these two encoding methods on a diverse set of hardware and software benchmarks, we conclude that neither method is robust to variations in formula characteristics. We propose a new hybrid technique that combines the two methods. We give experimental results showing that the hybrid method can significantly outperform either approach as well as other decision procedures. Categories and Subject Descriptors I.1 [Symbolic and Algebraic Manipulation]: Expressions and Their Representation, Algorithms; I.2.3 [Deduction and Theorem Proving]; F.4.1 [Mathematical Logic]: Mechanical theorem proving General Terms Algorithms, Experimentation, Measurement, Verification Keywords Design verification, Decision ...

• Type: Conference
• Year: 2003
• Where: DAC
• Authors: Sanjit A. Seshia, Shuvendu K. Lahiri, Randal E. Bryant
• Keywords: DAC 2003, Decision Procedures, Design Automation, Keywords Design Verification, SAT-based Decision Procedures