Combination of Decision Procedures
Summer School 2004

Cesare Tinelli

Topic: Nelson-Oppen combinations, latest advances including non-disjoint signatures, deterministic and non-deterministic algorithms, fusion methods.

• Lecture 1: PDF, Postscript
• Lecture 2: PDF, Postscript

Lecture 1

Title: The combination problem in unsorted first-order logic

We will start with a brief introduction to classical first-order logic and an overview of decision problems in this logic, and their combinations. We will discuss how decision problems for first-order theories can be defined as validity problems for certain classes of formulas, and survey a number of them. Then we will see that combinations of validity problems are in essence just interpolation problems, and that combining decision procedures amounts to computing interpolants, or proving their non-existence, in finite time.

We will concentrate on combining decision problems for universal formulas and discuss in detail the foremost combination method for such problems, originally due to Nelson and Oppen. We will see that it is possible to give a straightforward proof of correctness of the method by using a very simple and general model-theoretic result about interpolation problems.

This general result can also be used to relax the two main requirements of the Nelson-Oppen method: the "stable infiniteness" of the component theories and the disjointness of their signatures. We will discuss some possible extensions of the method, and their limitations, to theories that may not be stably infinite or that may share function or predicate symbols.

Lecture 2

Title: The combination problem in sorted first-order logics

The results presented in the first talk are framed in the context of unsorted first-order logic. However, in many of the application domains in which combination problems arise, using a sorted logic is more appropriate as these domains are naturally typed. This talk will deal with the issue of lifting known combination results to sorted versions of first-order logic.

We will first briefly introduce many-sorted logic and then extended it to a fairly general order-sorted logic (ie., a sorted logic with subsorts). Then we will argue that, while the main issues for the combination problems in sorted logics are the same as in the unsorted case, certain combination results are in a sense easier to obtain because of the restrictions imposed by the sorted language. We will do this by presenting a version of the Nelson-Oppen method for the given sorted logic and discussing its correctness and possible extensions.

References

• F. Baader and K. Schulz. Combining Constraint Solving. In H. Comon, C. Marché, and R. Treinen, editors, Constraints in Computational Logics, volume 2002 of Lecture Notes in Computer Science. SpringerVerlag, 2001.
• Franz Baader and Cesare Tinelli. Deciding the Word Problem in the Union of Equational Theories Sharing Constructors. Information and Computation, 178(2), 2002.
• Zohar Manna and Calogero G. Zarba. Combining decision procedures. In Formal Methods at the Cross Roads: From Panacea to Foundational Support, Volume 2757 of Lecture Notes in Computer Science, pages 381-422, Springer, 2003.
• Greg Nelson, Derek C. Oppen: Simplification by Cooperating Decision Procedures. ACM Trans. Program. Lang. Syst. 1(2): 245-257 (1979)
• Cesare Tinelli and Christophe Ringeissen. Unions of Non-Disjoint Theories and Combinations of Satisfiability Procedures. Theoretical Computer Science, 290(1), 2003.
• Cesare Tinelli and Calogero Zarba. Combining non-stably infinite theories. Submitted to JAR. 2004.
• Cesare Tinelli and Calogero Zarba. Combining decision procedures for theories in sorted logics. In Proceedings of the 9th European Conference on Logic in Artificial Intelligence (JELIA'04), Lisbon, Portugal, 2004.
• Calogero G. Zarba. C-tableaux. Technical Report RR-5229, INRIA, 2004.

Clark Barrett

Topic: CVC Lite + HOL light; Non-clausal decision heuristic; Partial functions.

Slides in PDF, Postscript,

Ashish Tiwari

Title: Abstract Congruence Closure, Binomial Ideals, and Algebraically Closed Fields

• Lecture 1
• Lecture 2

Abstract

References

• Leo Bachmair, Ashish Tiwari, and Laurent Vigneron, Abstract Congruence Closure, J. of Automated Reasoning 31(2), 2003, pp. 129--168, Kluwer Academic Publishers.
• L. Bachmair, I.V. Ramakrishnan, A. Tiwari, and L. Vigneron, Congruence Closure modulo Associativity and Commutativity, Workshop on Frontiers of Combining Systems, FroCos 2000 , LNAI 1794.
• Leo Bachmair and Ashish Tiwari, D-bases for Polynomial Ideals over Commutative Noetherian Rings, Rewriting Techniques and Applications, Proceedings of the 8th RTA-1997, pp. 113-127.
• Little Engines of Proof, Course Notes,
• Franz Baader and Tobias Nipkow, Term Rewriting and All That, Cambridge University Press, 1999.

Sergey Berezin

Title: CVC Lite: An Efficient Theorem Prover Based on Combination of Decision Procedures

Slides in PowerPoint.

Abstract

Validity checkers, which are theorem provers based on combination of efficient decision procedures, have become quite popular in the formal verification community in the recent years.

CVC Lite is an implementation of a validity checker for first-order logic with several interpreted theories such as equality, uninterpreted functions, arithmetic, and theory of arrays. It is a next generation tool developed upon our previous experience with SVC (Stanford Validity Checker) and CVC (Cooperating Validity Checker). The tool is designed to be very efficient, easy to use as a C++ library and as a stand-alone executable, and convenient to extend with new features, including new decision procedures.

In this talk, I will go over the underlying theory of CVC Lite, its high-level architecture, and some important features and design decisions. Specifically, the topics include:

• High-level architecture of the tool
• Equality reasoning with Union-Find and efficient setup/update mechanism
• Soundness: computing with proof rules, trusted codebase
• Integrated SAT solver
• Efficient backtracking mechanism
• Completeness of CVC Lite
• Conflict analysis in the presence of theories
• Support for partial functions and subtypes
• Support for quantifiers
• Proof production

References

• Clark Barrett and Sergey Berezin. CVC Lite: A New Implementation of the Cooperating Validity Checker. In Proceedings of CAV'04, July 2004
• Sergey Berezin, Clark Barrett, Igor Shikanian, Marsha Chechik, Arie Gurfinkel, and David L. Dill. A Practical Approach to Partial Functions in CVC Lite. In proceedings of PDPAR'04, July 2004
• Clark Barrett and Sergey Berezin. A Proof-Producing Boolean Search Engine. In Proceedings of PDPAR 2003 Workshop, Miami, Florida, USA, July, 2003.
• Clark W. Barret. Checking Validity of Quantifier-Free Formulas in Combinations of First-Order Theories. PhD Thesis, Stanford University, 2003.

Leonardo De Moura

Topic: ICS tool

Sanjit Seshia and Shuvendu Lahiri

Title: UCLID: Deciding Combinations of Theories via Eager Translation to SAT.

• Sanjit's part
• Shuvendu's part

Abstract

UCLID incorporates a decision procedure for a combination of the theories of uninterpreted functions and equality, integer linear arithmetic, and constrained lambda expressions (used to model arrays, e.g.). This procedure is unique among current SAT-based decision procedures in two ways. First, it is based on an "eager" translation to SAT; i.e., a translation of the input formula to a equi-satisfiable Boolean formula in a single step. Secondly, one of its encoding techniques is based on exploiting the "small-model" property for the theories handled.

In this talk, we will describe the following aspects of UCLID:

1. The logic supported by UCLID, starting with CLU logic [BLS02].
2. Exploiting robust positive equality [LBGT04] in handling uninterpreted functions.
3. Exploiting the small-model property for integer linear arithmetic [SB04] to construct an efficient decision procedure.
4. Tool architecture and design decisions.

We will also make theoretical and empirical comparisons with other decision procedures for the same logic.

UCLID website: http://www.cs.cmu.edu/~uclid

References

• [BLS02] R. E. Bryant, S. K. Lahiri, and S. A. Seshia, Modeling and Verifying Systems using a Logic of Counter Arithmetic with Lambda Expressions and Uninterpreted Functions , Computer-Aided Verification CAV'02, E. Brinksma and K. G. Larsen, eds., LNCS 2404, Springer-Verlag, July 2002, pp. 78-92.
• [LBGT04] S. K. Lahiri, R. E. Bryant, A. Goel, and M. Talupur Revisiting Positive Equality , Tools and Algorithms for the Construction and Analysis of Systems, TACAS'04, Lecture Notes in Computer Science 2988, Springer-Verlag, March 2004, pp. 1-15.
• [SB04] S. A. Seshia and R. E. Bryant, Deciding Quantifier-Free Presburger Formulas Using Parameterized Solution Bounds , IEEE Symposium on Logic in Computer Science LICS'04, IEEE Press, July 2004.
• [LS04] S. K. Lahiri and S. A. Seshia, The UCLID Decision Procedure , Computer-Aided Verification CAV'04, R. Alur and D. Peled, eds., LNCS 3114, Springer-Verlag, July 2004, pp. 475-478.

Rajeev Joshi

Title:Verifun: A Theorem Prover Using Lazy Proof Explication

Slides in PDF

Abstract

Theorem provers based on "cooperating decision procedures" have been used in program verification since they were first proposed by Nelson and Oppen in 1979. One such prover, `Simplify', was developed by Detlefs, Nelson and Saxe at the DEC/Compaq Systems Research Center (SRC) and used in a variety of program checking tools, including ESC/Modula-3, ESC/Java, Calvin, and Microsoft's SLAM tool. Experience with using Simplify over a number of years, however, pointed to two shortcomings in its design. First, the backtracking search used in Simplify for propositional inference had been far surpassed by modern SAT-solving techniques based on learning. Second, from each inconsistency detected by the theories, the backtracking search gained only one bit of information, viz, the infeasibility of the current assignment. This often led Simplify to discover the "same" inconsistencies repeatedly during a proof.

The `Verifun' theorem prover was developed at Compaq/HP SRC in order to overcome the shortcomings of Simplify. In contrast to Simplify, Verifun employed a new style of interaction in which the propositional search was performed by an independent SAT solver, and the theories explicated proofs at each encountered inconsistency, in order to prune multiple infeasible assignments at a time. Because of its intended use in program verification, Verifun was designed for formulae involving propositional logic, equality with uninterpreted function symbols, linear arithmetic and quantification. In this talk, I will describe the architecture of Verifun, discuss some key design choices, and relate some experiences with its performance.

This work was done jointly at SRC with Cormac Flanagan and Jim Saxe, with help from summer intern Simon Ou.

Sava Krstic

• Lecture 1
• Lecture 2

Lecture 1

Title: Combining Canonizers and Solvers

Abstract

References

• S. Krstic and S. Conchon, Canonization for Disjoint Union of Theories, Information and Computation (to appear)

Lecture 2

Abstract

References

• S. Conchon and S. Krstic, Strategies for Combining Decision Procedures, Theoretical Computer Science (to appear)

Harald Ruess

Topic: Modularity and Refinement of Inference Systems for Equality

Slides in PDF

Vijay Ganesh

Title:: Combination results for many sorted theories with overlapping signatures

Slides

• Lecture 1
• Lecture 2

In these talks, We will present a combination result for many-sorted first order theories whose signatures may share common symbols (i.e. overlapping or non-disjoint signatures), extending the recent results by Ghilardi for the unsorted case. The focus of the talks will be on three aspects of the result, namely

1. Conditions for consistency of the union theory
2. The combination procedure and its completeness
3. Decidability conditions

Lecture 1

In the first talk, we will motivate the problem, and present the key insights behind the notions (e.g. T0-compatibility) and theorems needed by this approach to establish consistency, completeness and decidability. We will also discuss the connection between T0-compatibility and stably-infiniteness of a theory.

Lecture 2

In the second talk, details of the proof constructions of the Union Consistency Theorem and the Union Completeness Theorem shall be presented. Time permitting, CVCL (CVC Lite) completeness result and decidability theorems will be discussed as well.

References

• Vijay Ganesh, Sergey Berezin, Cesare Tinelli, David L. Dill, Combination Results for Many Sorted Theories with Overlapping Signatures. Tech Report, Stanford University, 2004.
• Silvio Ghilardi. Model-Theoretic Methods in Combined Constraint Satisfiability. Journal of Automated Reasoning, to appear (2004).
• C. C. Chang and H. J. Keisler. Model Theory. Elsevier Science Ltd, 3rd edition, 1998.

Marco Maratea

Topic: TSAT++ theorem prover

Abstract

Separation Logic (SL) is a decidable logic combining Boolean logic with a fragment of linear arithmetic, able to compactly capture the behavior of a large class of infinite-state systems. It is not surprising, then, that recently a number of interesting problems of AI (planning, scheduling, temporal reasoning) and Formal Methods (safety of hardware, bounded model checking of real-time systems) have been recast as decision problems of SL-formulae. Hence, the need of efficient decision procedures for this logic. In this talk I present TSAT++, an efficient SAT-based decision procedure for Separation Logic implementing the lazy-approach. I will discuss about the TSAT++'s architecture as well as the optimization techniques (both borrowed from the AI and Formal Methods literature and new) implemented in it. Finally, I ll show some comparative evaluation against state-of-the-art systems on a wide range of benchmarks.

References

• A. Armando, C. Castellini, E. Giunchiglia, M. Idini, M. Maratea, TSAT++: An Open Reasoning Platform for Satisfiability Modulo Theory. Accepted to PDPAR 2004. 5 July 2004, Cork, Ireland.
• A. Armando, C. Castellini, E. Giunchiglia, M. Maratea, A SAT-based Decision Procedure for the Boolean Combination of Difference Constraints. Accepted to SAT 2004. 10-13 May, Vancouver, Canada.

Sumit Gulwani

Slides in PowerPoint

Topic: Randomized join algorithms for linear arithmetic and uninterpreted functions.

Abstract

Join algorithms can be seen as generalization of decision procedures. They are used in program analysis to merge the sets of facts at a join point. A join algorithm for a theory seems to be considerably harder to design than a decision procedure. Randomization may be used as a tool to obtain efficient and simpler join algorithms. In this talk, I will describe randomized join algorithms for the theory of linear arithmetic, and the theory of uninterpreted functions. I will also motivate and present the challenges behind the problem of making join algorithms context-sensitive, and the problem of combining join algorithms.

References

• Discovering Affine Equalities using Random Interpretation, Sumit Gulwani, George Necula, POPL 2003
• Global Value Numbering using Random Interpretation, Sumit Gulwani, George Necula, POPL 2004