Predicate learning and selective theory deduction for a difference logic solver

ABSTRACT

Design and verification of systems at the Register-Transfer (RT) or behavioral level require the ability to reason at higher levels of abstraction. Difference logic consists of an arbitrary Boolean combination of propositional variables and difference predicates and therefore provides an appropriate abstraction. In this paper, we present several new optimization techniques for efficiently deciding difference logic formulas. We use the lazy approach by combining a DPLL Boolean SAT procedure with a dedicated graph-based theory solver, which adds transitivity constraints among difference predicates on a "need-to" basis. Our new optimization techniques include flexible theory constraint propagation, selective theory deduction, and dynamic predicate learning. We have implemented these techniques in our lazy solver. We demonstrate the effectiveness of the proposed techniques on public benchmarks through a set of controlled experiments.

REFERENCES

• 1: A. Armando, C. Castellini, E. Giunchiglia, and M. Maratea. A SAT-based decision procedure for the boolean combination of difference constraints In Theory and Applications of Satisfiability Testing (SAT'04), pages 166--173, Vancouver, CA, May 2004.
• 2: Thomas Ball , Rupak Majumdar , Todd Millstein , Sriram K. Rajamani, Automatic predicate abstraction of C programs, Proceedings of the ACM SIGPLAN 2001 conference on Programming language design and implementation, p.203-213, June 2001, Snowbird, Utah, United States
• 3: 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
• 4: 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
• 5: Thomas T. Cormen , Charles E. Leiserson , Ronald L. Rivest, Introduction to algorithms, MIT Press, Cambridge, MA, 1990
• 6: S. Cotton. Satisfiability checking with difference constraints. Msc thesis, IMPRS Computer Science, Saarbrucken, 2005.
• 7: Martin Davis , George Logemann , Donald Loveland, A machine program for theorem-proving, Communications of the ACM, v.5 n.7, p.394-397, July 1962 [doi>10.1145/368273.368557]
• 8: Jean-Christophe Filliâtre , Sam Owre , Harald Rueß , Natarajan Shankar, ICS: Integrated Canonizer and Solver, Proceedings of the 13th International Conference on Computer Aided Verification, p.246-249, July 18-22, 2001
• 9: M. K. Ganai, M. Talupur, and A. Gupta. SDSAT: Tight integration of small domain encoding and lazy approaches in a separation logic solver. In Tools and Algorithms for the Construction and Analysis of Systems (TACAS'06), pages 135--150. Springer, 2006. LNCS 3920.
• 10: H. Ganzinger, G. Hagen, R. Nieuwenhuis, A. Oliveras, and C. Tinelli. DPLL(T): Fast decision procedures. In Computer-Aided Verification (CAV'04), pages 175--188. Springer, July 2004. LNCS 3114.
• 11: Thomas A. Henzinger , Ranjit Jhala , Rupak Majumdar , Grégoire Sutre, Lazy abstraction, Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.58-70, January 16-18, 2002, Portland, Oregon
• 12: T. A. Henzinger, X. Nicollin, J. Sifakis, and S. Yovine. Symbolic model checking for real-time systems. In IEEE International Symposium on Logic in Computer Science, pages 394--406, 1992.
• 13: H. Jain, F. Ivančić, A. Gupta, and M. Ganai. Localization and register sharing for predicate abstraction. In Tools and Algorithms for the Construction and Abnalysis of Systems (TACAS'05), pages 394--409. Springer, 2005. LNCS 3440.
• 14: S. Lahiri and S. Seshia. The UCLID decision procedure. In Computer Aided Verification (CAV'04), pages 475--478. Springer, 2004. LNCS 3114.
• 15: A. Koelbl , Yuan Lu , A. Mathur, Embedded tutorial: formal equivalence checking between system-level models and RTL, Proceedings of the 2005 IEEE/ACM International conference on Computer-aided design, p.965-971, November 06-10, 2005, San Jose, CA
• 16: M. Bozzano, R. Bruttomesso, A. Cimatti, T. Junttila, P. v. Rossum, S. Schulz, and R. Sebastiani. An incremental and layered procedure for the satisfiability of linear arithmetic logic. In Tools and Algorithms for the Construction and Analysis of Systems (TACAS'05), pages 317--333. Springer, 2005. LNCS 3440.
• 17: Matthew W. Moskewicz , Conor F. Madigan , Ying Zhao , Lintao Zhang , Sharad Malik, Chaff: engineering an efficient SAT solver, Proceedings of the 38th conference on Design automation, p.530-535, June 2001, Las Vegas, Nevada, United States [doi>10.1145/378239.379017]
• 18: R. Nieuwenhuis and A. Oliveras. DPLL(T) with exhaustive theory propagation and its application to difference logic. In Computer Aided Verification (CAV'05), pages 321--334. Springer, 2005. LNCS 3576.
• 19: G. Parthasarathy , M. K. Iyer , K. T. Cheng , F. Brewer, Structural search for RTL with predicate learning, Proceedings of the 42nd annual conference on Design automation, June 13-17, 2005, San Diego, California, USA [doi>10.1145/1065579.1065698]
• 20: Amir Pnueli , Yoav Rodeh , Ofer Strichmann , Michael Siegel, The small model property: how small can it be?, Information and Computation, v.178 n.1, p.279-293, October 10, 2002 [doi>10.1016/S0890-5401(02)93175-5]
• 21: G. Ramalingam, J. Song, L. Joscovicz, and R. Miller. Solving difference constraints incrementally. Algorithmica, 23(3):261--275, 1999.
• 22: Sanjit A. Seshia , Shuvendu K. Lahiri , Randal E. Bryant, A hybrid SAT-based decision procedure for separation logic with uninterpreted functions, Proceedings of the 40th conference on Design automation, June 02-06, 2003, Anaheim, CA, USA [doi>10.1145/775832.775945]
• 23: João P. Marques Silva , Karem A. Sakallah, GRASP—a new search algorithm for satisfiability, Proceedings of the 1996 IEEE/ACM international conference on Computer-aided design, p.220-227, November 10-14, 1996, San Jose, California, United States
• 24: 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
• 25: M. Talupur, N. Sinha, O. Strichman, and A. Pnueli. Range allocation for separation logic. In Computer-Aided Verification (CAV'04), pages 148--161. Springer, July 2004. LNCS 3114.
• 26: C. Wang, F. Ivančić, M. Ganai, and A. Gupta. Deciding separation logic formulae by SAT and incremental negative cycle elimination. In Logic for Programming Artificial Intelligence and Reasoning (LPAR'05), pages 322--336. Springer, 2005. LNCS 3835.

INDEX TERMS

Primary Classification:
  B. Hardware
  B.6 LOGIC DESIGN
      B.6.3 Design Aids
          Subjects: Verification

General Terms:
Algorithms, Verification

Keywords:
SAT, SMT solver, decision procedure, difference logic