FLoC '02 - CAV Monday July 29th

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-