CAV on Monday

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

Sessions take place in auditorium 1 unless otherwise indicated.

Invited talk

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.

Session 9: SAT Based Methods I

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.

Session 10: SAT Based Methods II

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.

Session 11: Symbolic Model Checking II

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.

Session 12: Tool Presentations I

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.

19:00-21:00  City Hall reception

Room: City Hall