CAV on Sunday

Detailed program
Sunday July 28th, 2002
See also the unified by-slot program

All sessions take place in auditorium 1.

Session 5: Symbolic Model Checking I

Chair: Edmund M. Clarke

08:45-09:00  Introduction and Welcome

09:00-09:30  Sharon Barner, IBM Haifa, Israel
Daniel Geist, IBM Haifa, Israel
Anna Gringauze, IBM Haifa, Israel
Symbolic localization reduction with reconstruction layering and backtracking
Localization reduction is an abstraction-refinement scheme for model checking which was introduced by Bob Kurshan as a means for tackling state explosion. It is completely automatic, but despite the work that has been done related to this scheme, it still suffers from computational complexity. In this paper we present algorithmic improvements to localization reduction that enabled us to overcome some of these problems. Namely, we present a new symbolic algorithm for path reconstruction including incremental refinement and backtracking. We have implemented these improvements and compared them to previous work on a large number of our industrial examples. In some cases the improvement was dramatic. Using these improvements we were able to verify circuits that we were not previously able to address.

09:30-10:00  Randal E. Bryant, Carnegie Mellon U, USA
Shuvendu K. Lahiri, Carnegie Mellon U, USA
Sanjit A. Seshia, Carnegie Mellon U, USA
Modeling and verifying systems using a logic of counter arithmetic with lambda expressions and uninterpreted functions
Verifiers for infinite-state systems must trade off between the expressiveness of the modeling formalism and the efficiency and automation of the tool. Efficient methods have been devised for specific classes of systems, such as superscalar processors and systems with arbitrary size queues. However, to model systems that are combinations of these classes, no one method works well enough.
In this paper, we present CLU, a logic of Counter arithmetic with Lambda expressions and Uninterpreted Functions. CLU generalizes the logic of equality with uninterpreted functions (EUF) that has proved useful for verifying pipelined processors. CLU includes, in addition to the constructs of EUF, constrained lambda expressions, ordering, and counter arithmetic. This allows us to model infinite-state systems, such as a variety of infinite memory structures, finite and infinite queues including lossy channels, and networks of identical processes. Even with this richer expressive power, the validity of a CLU formula can be efficiently decided by translating it to a propositional formula, and then using Boolean methods to check validity.
We have built UCLID, a system that can be used for checking safety properties of systems modeled in CLU. We demonstrate that UCLID is efficient and expressive, by modeling and verifying safety properties of a variety of systems, including an out-of-order execution unit and the load-store unit of an industrial microprocessor.

10:00-10:30  Sharon Barner, IBM Haifa, Israel
Orna Grumberg, Israel Inst. of Techn.
Combining symmetry reduction and under-approximation for symbolic model checking
This work presents a collection of methods, integrating symmetry reduction, under-approximation, and symbolic model checking in order to reduce space and time for model checking. The main goal of this work is falsification. However, under certain conditions our methods provide verification as well.
We first present algorithms that perform on-the-fly model checking for temporal safety properties, using symmetry reduction. We then extend these algorithm for checking liveness properties as well.
Our methods are fully automatic. The user should supply some basic information about the symmetry in the verified system. However, the methods are robust and work correctly even if the information supplied by the user is incorrect. Moreover, the methods return correct results even in case the computation of the symmetry reduction has not been completed due to memory or time explosion.
We implemented our methods within IBM's model checker RuleBase, and compared the performance of our methods with that of RuleBase. In most cases, our algorithms outperformed RuleBase with respect to both time and space.

Session 6: Abstraction and Refinement

Chair: Robert Kurshan

11:00-11:30  Amir Pnueli, Weizmann Inst. of Science, Israel
Jessie Xu, New York U, USA
Lenore Zuck, New York U, USA
Liveness with (0,1,infinity)-counter abstraction
We introduce the (0,1,infinity)-counter abstraction method by which a parameterized system of unbounded size is abstracted into a finite-state system. Assuming that each process in the parameterized system is finite-state, the abstract variables are limited counters which count, for each local state s of a process, the number of processes which currently are in local state s. The counters are saturated at 2, which means that counter(s)=2 whenever 2 or more processes are at state s. The emphasis of the paper is on the derivation of an adequate and sound set of fairness requirements (both weak and strong) which enable proofs of liveness properties of the abstract system, from which we can safely conclude a corresponding liveness property of the original parameterized system. We illustrate the method on few parameterized systems, including Szymanski's Algorithm for mutual exclusion.
The method is then extended to deal with parameterized systems whose processes may have infinitely many local states, such as the Bakery Algorithm. The extension is based on a choice of few "interesting" and "relevant" state assertions and then (0,1,infinity)-counting the number of processes satisfying each of these assertions.

11:30-12:00  Prosenjit Chatterjee, U Utah, USA
Hemanthkumar Sivaraj, U Utah, USA
Ganesh Gopalakrishnan, U Utah, USA
Shared memory consistency protocol verification against weak memory models: refinement via model-checking
Weak shared memory consistency models, especially those used by modern microprocessor families, are quite complex. The bus and/or directory-based protocols that help realize shared memory multiprocessors using these microprocessors are also exceedingly complex. Thus, the correctness problem - that all the executions generated by the multiprocessor for any given concurrent program are also allowed by the memory model - is a major challenge. In this paper, we present a formal approach to verify protocol implementation models against weak shared memory models through automatable refinement checking supported by a model checker. We define a taxonomy of weak shared memory models that includes most published commercial memory models, and detail how our approach applies over all these models. In our approach, the designer follows a prescribed procedure to build a highly simplified intermediate abstraction for the given implementation. The intermediate abstraction and the implementation are concurrently run using a model-checker, checking for refinement. The intermediate abstraction can be proved correct against the memory model specification using theorem proving. We have verified four different Alpha memory model implementations and two different Itanium memory model implementations against their respective specifications. The results are encouraging in terms of the uniformity of the procedure, the high degree of automation, acceptable run-times, and empirically observed bug-hunting efficacy. The use of parallel model-checking, based on a version of the parallel Murφ model checker we have recently developed for the MPI library, has been essential to finish the search in a matter of a few hours.

12:00-12:30  Patrice Godefroid, Bell Labs, USA
Radha Jagadeesan, Loyola U Chicago, USA
Automatic abstraction using generalized model checking
Generalized model checking is a framework for reasoning about partial state spaces of concurrent reactive systems. The state space of a system is only "partial" (partially known) when a full state-space exploration is not computationally tractable, or when abstraction techniques are used to simplify the system's representation. In the context of automatic abstraction, generalized model checking means checking whether there exists a concretization of an abstraction that satisfies a temporal logic formula. In this paper, we show how generalized model checking can extend existing automatic abstraction techniques (such as predicate abstraction) for model checking concurrent/reactive programs and yield the three following improvements: (1) any temporal logic formula can be checked (not just universal properties as with traditional conservative abstractions), (2) correctness proofs and counter-examples are both guaranteed to be sound, and (3) verification results can be more precise. We study the cost needed to improve precision by presenting new upper and lower bounds for the complexity of generalized model checking in the size of the abstraction.

Session 7: Compositional Verification I

Chair: Thomas A. Henzinger

14:00-14:30  Jason Baumgartner, IBM Enterprise Systems Group, USA
Andreas Kuehlmann, Cadence Design Systems, USA
Jacob Abraham, U Texas-Austin, USA
Property checking via structural analysis
This paper describes a framework for "structural target enlargement". Our approach is based upon a structural decomposition of the verification problem into several subtasks, each solved by a specialized algorithm for overall efficiency. Our contributions include the following: (1) a robust backward unfolding technique for structural target enlargement: from the target states, we perform "compose-based" pre-image computations for a number of steps determined by structural analysis, truncating the search if resource limitations are exceeded; (2) similar to frontier simplification in symbolic reachability analysis, we describe the application of don't cares for enhancing the presented target enlargement; and (3) a structural algorithm for computing a bound of a state-transition diagram's diameter which, for several classes of industrial designs, is sufficiently small to guarantee completeness of a bounded model check. In most cases, the verification problem is efficiently discharged by the enlargement process; otherwise, it is passed in simplified form to another solution approach. The presented techniques are implemented in a flexible verification framework that allows arbitrary combination with other techniques. Extensive experimental results demonstrate the effectiveness of the described methods.

14:30-15:00  Sriram K. Rajamani, Microsoft Research, USA
Jakob Rehof, Microsoft Research, USA
Conformance checking for models of asynchronous message passing software
We propose a notion of conformance between a specification S and an implementation model I extracted from a message-passing program. In our framework, S and I are CCS processes, which soundly abstract the externally visible communication behavior of a message-passing program. We use the extracted models to check that programs do not get stuck, waiting to receive or trying to send messages in vain. We show that our definition of stuckness and conformance capture important correctness conditions of message-passing software. Our definition of conformance was motivated by the need for modular reasoning over models, leading to the requirement that conformance preserve substitutability with respect to stuck-freeness: If I conforms to S, and P is any environment such that P|S is stuck-free, then it follows that P|I is stuck-free. We present an algorithm for checking if I conforms to S, discuss implementation of the algorithm, and present experience on some examples.

15:00-15:30  Cormac Flanagan, Compaq, USA
Shaz Qadeer, Compaq, USA
Sanjit Seshia, Compaq, USA
A modular checker for multithreaded programs
Ensuring the reliability of multithreaded software systems through testing is difficult, because of nondeterministic and subtle interactions between threads. Static checking, which has the potential to analyze the program's behavior over all execution paths and for all thread interleavings, is a promising complementary technique. We have built a scalable and expressive static checker called Calvin for multithreaded programs. To handle realistic programs, Calvin performs modular checking of each procedure called by a thread using specifications of other procedures and other threads. The checker leverages off existing techniques based on verification conditions and automatic theorem proving.
To evaluate the checker, we have applied it to several real-world programs. Our experience indicates that Calvin has a moderate annotation overhead and can catch defects in multithreaded programs, including synchronization errors and violation of data invariants.

Session 8: Timing Analysis

Chair: Doron A. Peled

16:00-16:30  Tomohiro Yoneda, Tokyo Inst. of Techn., Japan
Tomoya Kitai, Tokyo Inst. of Techn., Japan
Chris Myers, U Utah, USA
Automatic derivation of timing constraints by failure analysis
This work proposes a technique to automatically obtain timing constraints for a given timed circuit to operate correctly. A designated set of delay parameters of a circuit are first set to sufficiently large bounds, and verification runs followed by failure analysis are repeated. Each verification run performs timed state space enumeration under the given delay bounds, and produces a failure trace if it exists. The failure trace is analyzed, and sufficient timing constraints to prevent the failure is obtained. Then, the delay bounds are tightened according to the timing constraints by using a ILP (Integer Linear Programming) solver. This process terminates when either some delay bounds under which no failure is detected are found or no new delay bounds to prevent the failures can be obtained. The experimental results using a naive implementation show that the proposed method can efficiently handle asynchronous benchmark circuits and nontrivial GasP circuits.

16:30-17:00  Ofer Strichman, Carnegie Mellon U, USA
Sanjit A. Seshia, Carnegie Mellon U, USA
Randal E. Bryant, Carnegie Mellon U, USA
Reducing linear inequalities to propositional formulas
We show a reduction to propositional logic from a Boolean combination of inequalities of the form vivj+c and vi>vj+c, where c is a constant and vi,vj are variables of type real or integer. Equalities and uninterpreted functions can be expressed in this logic as well. We discuss the advantages of using this reduction as compared to competing methods, and present experimental results that support our claims.

17:00-17:30  Hakan L. S. Younes, Carnegie Mellon U, USA
Reid G. Simmons, Carnegie Mellon U, USA
Probabilistic verification of descrete event systems using acceptance sampling
We present a procedure for verifying properties of discrete event systems modeled as generalized semi-Markov processes. The dynamics of such systems can be very complex, which makes them hard to analyze. We resort to methods based on Monte Carlo simulation and statistical hypothesis testing. The verification is probabilistic in two senses. First, the properties, expressed as CSL formulas interpreted over generalized semi-Markov processes, can be probabilistic. Second, the result of the verification is probabilistic, and the probability of error is bounded by two parameters passed to the verification procedure. The verification of properties can be carried out in an anytime manner by starting off with loose error bounds, and gradually tightening these bounds.