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

ABSTRACT

SAT-based decision procedures for quantifier-free fragments of first-order 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 therefore 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.

REFERENCES

• 1: Gilles Audemard , Piergiorgio Bertoli , Alessandro Cimatti , Artur Kornilowicz , Roberto Sebastiani, A SAT Based Approach for Solving Formulas over Boolean and Linear Mathematical Propositions, Proceedings of the 18th International Conference on Automated Deduction, p.195-210, July 27-30, 2002
• 2: Clark W. Barrett , David L. Dill , Jeremy R. Levitt, Validity Checking for Combinations of Theories with Equality, Proceedings of the First International Conference on Formal Methods in Computer-Aided Design, p.187-201, November 06-08, 1996
• 3: Clark W. Barrett , David L. Dill , Aaron Stump, Checking Satisfiability of First-Order Formulas by Incremental Translation to SAT, Proceedings of the 14th International Conference on Computer Aided Verification, p.236-249, July 27-31, 2002
• 4: Randal E. Bryant , Steven German , Miroslav N. Velev, Processor verification using efficient reductions of the logic of uninterpreted functions to propositional logic, ACM Transactions on Computational Logic (TOCL), v.2 n.1, p.93-134, Jan. 2001 [doi>10.1145/371282.371364]
• 5: R. E. Bryant, S. K. Lahiri, and S. A. Seshia. Deciding CLU logic formulas via Boolean and pseudo-Boolean encodings. In Constraints in Formal Verification CFV'02.
• 6: Randal E. Bryant , Shuvendu K. Lahiri , Sanjit A. Seshia, Modeling and Verifying Systems Using a Logic of Counter Arithmetic with Lambda Expressions and Uninterpreted Functions, Proceedings of the 14th International Conference on Computer Aided Verification, p.78-92, July 27-31, 2002
• 7: Randal E. Bryant , Miroslav N. Velev, Boolean Satisfiability with Transitivity Constraints, Proceedings of the 12th International Conference on Computer Aided Verification, p.85-98, July 15-19, 2000
• 8: Jerry R. Burch , David L. Dill, Automatic verification of Pipelined Microprocessor Control, Proceedings of the 6th International Conference on Computer Aided Verification, p.68-80, June 21-23, 1994
• 9: Satyaki Das , David L. Dill , Seungjoon Park, Experience with Predicate Abstraction, Proceedings of the 11th International Conference on Computer Aided Verification, p.160-171, July 06-10, 1999
• 10: Thomas A. Henzinger , Ranjit Jhala , Rupak Majumdar , George C. Necula , Grégoire Sutre , Westley Weimer, Temporal-Safety Proofs for Systems Code, Proceedings of the 14th International Conference on Computer Aided Verification, p.526-538, July 27-31, 2002
• 11: Shuvendu K. Lahiri , Sanjit A. Seshia , Randal E. Bryant, Modeling and Verification of Out-of-Order Microprocessors in UCLID, Proceedings of the 4th International Conference on Formal Methods in Computer-Aided Design, p.142-159, November 06-08, 2002
• 12: Amir Pnueli , Yoav Rodeh , Ofer Shtrichman , Michael Siegel, Deciding Equality Formulas by Small Domains Instantiations, Proceedings of the 11th International Conference on Computer Aided Verification, p.455-469, July 06-10, 1999
• 13: A. Pnueli, M. Siegel, and O. Shtrichman. The code validation tool (CVT) - automatic verification of a compilation process. Software Tools for Technology Transfer, 2, 1998, pages 192--201.
• 14: Ofer Strichman , Sanjit A. Seshia , Randal E. Bryant, Deciding Separation Formulas with SAT, Proceedings of the 14th International Conference on Computer Aided Verification, p.209-222, July 27-31, 2002
• 15: Miroslav N. Velev , Randal E. Bryant, Effective use of boolean satisfiability procedures in the formal verification of superscalar and VLIW, Proceedings of the 38th conference on Design automation, p.226-231, June 2001, Las Vegas, Nevada, United States [doi>10.1145/378239.378469]

INDEX TERMS

Primary Classification:
  I. Computing Methodologies
  I.1 SYMBOLIC AND ALGEBRAIC MANIPULATION
      I.1.1 Expressions and Their Representation

Additional Classification:
  F. Theory of Computation
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.1 Mathematical Logic
          Subjects: Mechanical theorem proving

  I. Computing Methodologies
  I.1 SYMBOLIC AND ALGEBRAIC MANIPULATION
      I.1.2 Algorithms
  I.2 ARTIFICIAL INTELLIGENCE
      I.2.3 Deduction and Theorem Proving

General Terms:
Algorithms, Experimentation, Measurement, Verification

Keywords:
boolean satisfiability, decision procedures, design verification, theorem proving