| | Sessions
take place in auditorium 1 unless otherwise indicated.Joint
with CADE 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
| Clark W. Barrett, Stanford U, USA David
L. Dill, Stanford U, USA Aaron
Stump, Stanford U, USA
**Checking
satisfiability of first-order formulas by incremental
translation to SAT**
In the past few years, general-purpose propositional
satisfiability (SAT) solvers have improved dramatically in performance and
have been used to tackle many new problems. It has also been shown that
certain simple fragments of first-order logic can be decided efficiently by
first translating the problem into an equivalent SAT problem and then using
a fast SAT solver. In this paper, we describe an alternative but similar
approach to using SAT in conjunction with a more expressive fragment of
first-order logic. However, rather than translating the entire formula up
front, the formula is incrementally translated during a search for the
solution. As a result, only that portion of the translation that is
actually relevant to the solution is obtained. We describe a number of
obstacles that had to be overcome before developing an approach which was
ultimately very effective, and give results on verification benchmarks
using CVC (Cooperating Validity Checker) and the Chaff SAT solver. The
results show a performance gain of several orders of magnitude over CVC
alone and indicate that the method is more robust than the heuristics found
in CVC's predecessor, SVC. |
*Chair:*
David Basin
11:00- | 11:30
| Ken L. McMillan, Cadence Design Systems, USA
**Applying
SAT methods in unbounded symbolic model checking**
A method of symbolic model checking is introduced that uses
conjunctive normal form (CNF) rather than binary decision diagrams (BDD's)
and uses a SAT-based approach to quantifier elimination. This method is
compared to a traditional BDD-based model checking approach using a set of
benchmark problems derived from the compositional verification of a
commercial microprocessor design. |
11:30- | 12:00
| Edmund M. Clarke, Carnegie Mellon U, USA Anubhav
Gupta, Carnegie Mellon U, USA James
Kukula, Synopsis, USA Ofer
Strichman, Carnegie Mellon U, USA
**SAT
based abstraction-refinement using ILP and machine learning
techniques**
We describe new techniques for model checking in the
counterexample guided abstraction/refinement framework. The abstraction
phase `hides' the logic of various variables, hence considering them as
inputs. This type of abstraction may lead to `spurious' counterexamples,
i.e. traces that can not be simulated on the original (concrete) machine.
We check whether a counterexample is real or spurious with a SAT checker.
We then use a combination of Integer Linear Programming (ILP) and machine
learning techniques for refining the abstraction based on the
counterexample. The process is repeated until either a real counterexample
is found or the property is verified. We have implemented these techniques
on top of the model checker NuSMV and the SAT solver Chaff. Experimental
results prove the viability of these new techniques. |
12:00- | 12:30
| Jesse D. Bingham, U British Columbia, Canada Alan
J. Hu, U British Columbia, Canada
**Semi-formal
bounded model checking**
This paper presents a novel approach to bounded model checking.
We replace the SAT solver by an extended simulator of the circuit being
verified. Compared to SAT-solving algorithms, our approach sacrifices some
generality in selecting splitting variables and in the kinds of learning
possible. In exchange, our approach enables compiled simulation of the
circuit being verified, while our simulator extension allow us to retain
limited learning and conflict-directed backtracking. The result combines
some of the raw speed of compiled simulation with some of the search-space
pruning of SAT solvers. On example circuits, our preliminary implementation
is competitive with state-of-the-art SAT solvers, and we provide intuition
for when one method would be superior to the other. More importantly, our
verification approach continuously knows its coverage of the search space,
providing useful semi-formal verification results when full verification is
infeasible. In some cases, very high coverage can be attained in a tiny
fraction of the time required for full coverage by either our approach or
SAT solving. |
*Chair:*
Ken McMillan
14:00- | 14:30
| Marco Bozzano, ITC-irst, Italy Giorgio
Delzanno, U Genova, Italy
**Algorithmic
verification of invalidation-based protocols** Invalidation-based
protocols are widely used for ensuring the
consistency of data distributed on several nodes as in multi-processors
systems, and distributed file and database systems. The Broadcast Protocols
of Emerson and Namjoshi [EN98] represent a possible formal model one can
use here to specify systems with a finite but unbounded number of
finite-state components. The symbolic backward reachability algorithm of
Esparza, Finkel and Mayr can be used for checking, fully automatically,
safety properties for this class of infinite-state systems. This paradigm
has however the following limitation: it requires a preliminary (often
manual) step to abstract the behavior of individual processes into a
finite-state system. |
14:30- | 15:00
| Christian Jacobi, Saarland U, Germany
**Formal
verification of complex out-of-order pipelines by combining
model-checking and theorem-proving**
We describe a methodology for the formal verification of complex
out-of-order pipelines as they may be used as execution units in
out-of-order processors. The pipelines may process multiple instructions
simultaneously, may have branches and cycles in the pipeline structure, may
have variable latency, and may reorder instructions internally. The
methodology combines model-checking for the verification of the pipeline
control, and theorem proving for the verification of the pipeline
functionality. In order to combine both techniques, we formally verify that
the FairCTL operators defined in µ-calculus match
their intended semantics expressed in a form where computation traces are
explicit, since this form is better suited for theorem proving. This allows
the formally safe translation of model-checked properties of the pipeline
control into a theorem-proving friendly form, which is used for the
verification of the overall correctness of the pipeline, including
functional correctness. As an example we prove the correctness of the
pipeline of a multiplication/division floating point unit with all the
features mentioned above. |
15:00- | 15:30
| Yannick Chevalier, LORIA Nancy, France Laurent
Vigneron, LORIA Nancy, France
**Automated
unbounded verification of security protocols**
We present a new model for automated verification of security
protocols, permitting the use of an unbounded number of protocol runs. We
prove its correctness, completeness and also that it terminates. It has
been implemented and its efficiency is clearly shown by the number of
protocols successfully studied. In particular, we present an attack
previously unreported on the Denning-Sacco symmetric key
protocol. |
*Chair:*
Armin Biere
16:00- | 16:15
| Rajeev Alur, U Pennsylvania, USA Michael
McDougall, U Pennsylvania, USA Zijiang
Yang, U Pennsylvania, USA
**Exploiting
behavioral hierarchy for efficient model checking**
Software modeling languages use hierarchical state machines for
structured specification of control flow. This paper presents techniques
for exploiting the hierarchical structure for reducing the computational
requirements of algorithms for state-space exploration. We first report on
a tool called Hermes for creating and manipulating hierarchical models.
Then, we propose heuristics for both enumerative and BDD-based symbolic
algorithms for model checking. We demonstrate the benefits of our
heuristics using case-studies in analysis of network protocols and of
benchmark sequential circuits. |
16:15- | 16:30
| Marius Bozga, IMAG Grenoble, France Susanne
Graf, IMAG Grenoble, France Laurent
Mounier, IMAG Grenoble, France
**IF-2.0:
A validation environment for component-based real-time
systems**
The development of the IF toolbox was initiated several years
ago, in order to provide an open validation platform for timed asynchronous
systems (such as telecommunication protocols or distributed applications).
Despite the interest of this toolbox on specific applications, it appears
that some of the initial design choices, which were made to obtain a
maximal efficiency, are sometimes too restrictive. This situation motivated
the extension of the IF intermediate representation and, consequently, to
re-consider the architecture of its exploration engine. |
16:30- | 16:45
| Alessandro Armando, U Genova, Italy
*et al.*
**The
AVISS security protocols analysis tool**
We introduce AVISS, a tool for security protocol analysis that
supports the integration of back-ends implementing different search
techniques, allowing their systematic and quantitative comparison and
paving the way to their effective interaction. As a significant example, we
have implemented three back-ends, and then used the AVISS tool to analyze
30 of the 50 problems in the Clark-Jacob's protocol library. |
16:45- | 17:00
| Eugene Asarin, IMAG Grenoble, France Gordon
Pace, INRIA Rhône-Alpes, France Gerardo
Schneider, IMAG Grenoble, France Sergio
Yovine, IMAG Grenoble, France
**SPeeDI
- a verification tool for polygonal
hybrid systems**
We present a prototype tool SPeeDI for solving the reachability
problem for a class of planar hybrid systems: polygonal differential
inclusions. The tool implements our reachability algorithm combining
several techniques, namely, (1) the representation of the two-dimensional
continuous dynamics as a one-dimensional discrete dynamical system, (2) the
characterization of the set of qualitative behaviors of the latter as a
finite set of types of signatures, and (3) the "acceleration" of the
iterations in the case of cyclic signatures. The tool, programmed in
Haskell, decides reachability, calculates traces, and genrates graphical
representations of systems and traces. |
17:00- | 17:15
| Alessandro Cimatti, ITC-irst, Italy
*et al.*
**NuSMV2:
an opensource tool for symbolic model checking**
NuSMV is a symbolic model checker originated from the
reengineering, reimplementation and extension of SMV, the first BDD-based
model checker developed at CMU. The NuSMV project aims at the development
of a state-of-the-art symbolic model checker, designed to be applicable in
technology transfer projects, well structured, open, flexible and
documented.
This paper describes NuSMV version 2. NuSMV2 inherits all
the functionalities of the previous version, and extends them in several
directions. The main novelty in NuSMV2 is the integration of model checking
techniques based on propositional satisfiability (SAT), that are currently
enjoying a substantial success in several industrial fields. To the best of
our knowledge, NuSMV2 is currently the only publicly available system that
provides an effective integration of BDD-based and SAT-based model
checking.
With NuSMV2, we are also adopting a new development and
license model. NuSMV2 is distributed under the LGPL OpenSource license,
that allows anyone interested to freely use the tool and to participate in
its development. The aim of the NuSMV OpenSource project is to provide to
the model checking community a common platform for the research, the
implementation, and the comparison of new symbolic model checking
techniques. |
17:15- | 17:30
| Eugene Asarin, IMAG Grenoble, France Thao
Dang, IMAG Grenoble, France Oded
Maler, IMAG Grenoble, France
**The
d/dt tool for verification of hybrid systems**
In this paper we describe the tool d/dt which provides automatic
verification of safety properties of hybrid systems with linear continuous
dynamics with uncertain input. The verification procedure is based on a
method for over-approximating reachable sets by orthogonal polyhedra. In
addition, using reachability analysis the tool allows to automatically
synthesize a controller which switches the system between continuous modes
in order to satisfy a safety specification. |
Joint
with CADE, ICLP, TABLEAUX
*Room:*
City Hall | |