CADE on Monday

Detailed program
Monday July 29th, 2002
See also the unified by-slot program

Sessions take place in auditorium 3 unless otherwise indicated.

Invited talk

Joint with CAV
Room: auditorium 1

09:00-10:00  Sharad Malik, Princeton U, USA
Invited talk: The quest for efficient Boolean satisfiability solvers
The classical NP-complete problem of Boolean Satisfiability (SAT) has seen much interest in not just the theoretical computer science community, but also in areas where practical solutions to this problem enable significant practical applications. Since the first development of the basic search based algorithm proposed by Davis, Putnam, Logemann and Loveland (DPLL) about forty years ago, this area has seen active research effort with many interesting contributions that have culminated in state-of-the-art SAT solvers today being able to handle problem instances with thousands, and in same cases even millions, of variables. In this paper we examine some of the main ideas along this passage that have led to our current capabilities. Given the depth of the literature in this field, it is impossible to do this in any comprehensive way; rather we focus on techniques with consistent demonstrated efficiency in available solvers. For the most part, we focus on techniques within the basic DPLL search framework, but also briefly describe other approaches and look at some possible future research directions.

Session 9

10:00-10:30  Cristina Borralleras, U Vic, Spain
Salvador Lucas, Polytechnic U of Valencia, Spain
Albert Rubio, Techn. U of Catalonia, Spain
Recursive path orderings can be context-sensitive
Context-sensitive rewriting (CSR) is a simple restriction of rewriting which can be used e.g. for modelling non-eager evaluation in programming languages. Many times termination is a crucial property for program verification. Hence, developing tools for automatically proving termination of CSR is necessary. All known methods for proving termination of (CSR) systems are based on transforming the CSR system → into a (standard) rewrite system →' whose termination implies the termination of the CSR system →. In this paper first several negative results on the applicability of existing transformation methods are provided. Second, as a general-purpose way to overcome these problems, we develop the first (up to our knowledge) method for proving directly termination of context-sensitive rewrite systems: the context sensitive recursive path ordering (CSRPO). Many interesting (realistic) examples that cannot be proved or are hard to prove with the known transformation methods are easily handled using CSRPO. Moreover, CSRPO is very suitable for automation.

Session 10: Combination of Decision Procedures

11:00-11:30  Harald Ganzinger, MPI Saarbrücken, Germany
Shostak light
We represent the essential ingredients of Shostak's procedure at a high level of abstraction, and as a refinement of the Nelson-Oppen procedure. We analyze completeness issues of the method based on a general notion of theories. We also formalize a notion of σ-models and show that on the basis of Shostak's procedure we cannot distinguish a theory from its approximation represented by the class of its σ-models.

11:30-12:00  Jonathan Ford, U New England, Australia
Natarajan Shankar, SRI International, USA
Formal verification of a combination decision procedure
Decision procedures for combinations of theories are at the core of many modern theorem provers such as ACL2, Ehdm, PVS, SIMPLIFY, the Stanford Pascal Verifier, STeP, SVC, and Z/Eves. Shostak, in 1984, published a decision procedure for the combination of canonizable and solvable theories. Recently, Ruess and Shankar showed Shostak's method to be incomplete and nonterminating, and presented a correct version of Shostak's algorithm along with informal proofs of termination, soundness, and completeness. We describe a formalization and mechanical verification of these proofs using the PVS verification system. The formalization itself posed significant challenges and the verification revealed some gaps in the informal argument.

12:00-12:30  Calogero G. Zarba, Stanford U, USA
Combining multisets with integers
We present a decision procedure for a constraint language combining multisets of ur-elements, the integers, and an arbitrary first-order theory T of the ur-elements. Our decision procedure is an extension of the Nelson-Oppen combination method specifically tailored to the combination domain of multisets, integers, and ur-elements.

Session 11: Logical frameworks

14:00-14:30  Lawrence C. Paulson, U Cambridge, UK
The reflection theorem: A study in formalizing meta-theoretic reasoning
The reflection theorem has been proved using Isabelle/ZF. This theorem cannot be expressed in ZF, and its proof requires reasoning at the meta-level. There is a particularly elegant proof that reduces the meta-level reasoning to a single induction over formulas. Each case of the induction has been proved with Isabelle/ZF, whose built-in tools can prove specific instances of the reflection theorem upon demand.

14:30-15:00  Aaron Stump, Stanford U, USA
David L. Dill, Stanford U, USA
Faster proof checking in the Edinburgh Logical Framework
This paper describes optimizations for checking proofs represented in the Edinburgh Logical Framework (LF). The optimizations allow large proofs to be checked efficiently which cannot feasibly be checked using the standard algorithm for LF. The crucial optimization is a form of result caching. To formalize this optimization, a path calculus for LF is developed and shown equivalent to a standard calculus.

15:00-15:30  Chad E. Brown, Carnegie Mellon U, USA
Solving for set variables in higher-order theorem proving
In higher-order logic, we must consider literals with flexible (set variable) heads. Set variables may be instantiated with logical formulas of arbitrary complexity. An alternative to guessing the logical structures of instantiations for set variables is to solve for sets satisfying constraints. Using the Knaster-Tarski Fixed Point Theorem, constraints whose solutions require recursive definitions can be solved as fixed points of monotone set functions. In this paper, we consider an approach to higher-order theorem proving which intertwines conventional theorem proving in the form of mating search with generating and solving set constraints.

Session 12: Model checking

16:00-16:30  Orna Kupferman, Hebrew U of Jerusalem, Israel
Ulrike Sattler, Dresden U of Techn., Germany
Moshe Y. Vardi, Rice U, USA
The complexity of the graded µ-calculus
In classical logic, existential and universal quantifiers express that there exists at least one individual satisfying a formula, or that all individuals satisfy a formula. In many logics, these quantifiers have been generalized to express that, for a non-negative integer n, at least n individuals or all but n individuals satisfy a formula. In modal logics, graded modalities generalize standard existential and universal modalities in that they express, e.g., that there exist at least n accessible worlds satisfying a certain formula. Graded modalities are useful expressive means in knowledge representation; they are present in a variety of other knowledge representation formalisms closely related to modal logic. A natural question that arises is how the generalization of the existential and universal modalities affects the satisfiability problem for the logic and its computational complexity, especially when the numbers in the graded modalities are coded in binary. In this paper we study the graded µ-calculus, which extends graded modal logic with fixed-point operators, or, equivalently, extends classical µ-calculus with graded modalities. We prove that the satisfiability problem for graded µ-calculus is EXPTIME-complete - not harder than the satisfiability problem for µ-calculus, even when the numbers in the graded modalities are coded in binary.

16:30-17:00  Leonardo de Moura, SRI International, USA
Harald Rueß, SRI International, USA
Maria Sorea, SRI International, USA
Lazy theorem proving for bounded model checking over infinite domains
We investigate the combination of propositional SAT checkers with domain-specific theorem provers as a foundation for bounded model checking over infinite domains. Given a program M over an infinite state type, a linear temporal logic formula ϕ with domain-specific constraints over program states, and an upper bound k, our procedure determines if there is a falsifying path of length k to the hypothesis that M satisfies the specification ϕ. This problem can be reduced to the satisfiability of Boolean constraint formulas. Our verification engine for these kinds of formulas is lazy in that propositional abstractions of Boolean constraint formulas are incrementally refined by generating lemmas on demand from an automated analysis of spurious counterexamples using theorem proving. We exemplify bounded model checking for timed automata and for RTL level descriptions, and investigate the lazy integration of SAT solving and theorem proving.

17:00-18:00  CADE business meeting

19:00-21:00  City Hall reception

Room: City Hall