| | All
sessions take place in auditorium 1.*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. |
*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. |
*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. |
*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 *v*_{i}≥*v*_{j}+*c*
and *v*_{i}>*v*_{j}+*c*,
where *c* is a constant and *v*_{i},*v*_{j} 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. |
| |