| | Sessions
take place in auditorium 3 unless otherwise indicated.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. |
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. |
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. |
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. |
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. |
Joint
with CAV, ICLP, TABLEAUX
*Room:*
City Hall | |