| | Sessions
take place in auditorium 1 unless otherwise indicated.*Chair:*
Fabio Somenzi
09:00- | 09:30
| Orna Kupferman, Hebrew U of Jerusalem, Israel Nir
Piterman, Weizmann Inst. of Science, Israel Moshe
Y. Vardi, Rice U, USA
**Model
checking linear properties of prefix-recognizable
systems**
We develop an automata-theoretic framework for reasoning about
linear properties of infinite-state sequential systems. Our framework is
based on the observation that states of such systems, which carry a finite
but unbounded amount of information, can be viewed as nodes in an infinite
tree, and transitions between states can be simulated by finite-state
automata. Checking that the system satisfies a temporal property can then
be done by an alternating two-way automaton that navigates through the
tree. For branching properties, the framework is known and the two-way
alternating automaton is a tree automaton. Applying the framework for
linear properties results in algorithms that are not optimal. Indeed, the
fact that a tree automaton can split to copies and simultaneously read all
the paths of the tree has a computational price and is irrelevant for
linear properties. We introduce path automata on trees. The input to a path
automaton is a tree, but the automaton cannot split to copies and it can
read only a single path of the tree. In particular, two-way
nondeterministic path automata enable exactly the type of navigation that
is required in order to check linear properties of infinite-state
sequential systems.
As has been the case with finite-state systems,
the automata-theoretic framework is quite versatile. We demonstrate it by
solving several versions of the model-checking problem for LTL
specifications and prefix-recognizable systems. Our algorithm is
exponential in both the size of (the description of) the system and the
size of the LTL specification, and we prove a matching lower bound. This is
the first optimal algorithm for solving the LTL model-checking problem for
prefix recognizable systems. Our framework also handles systems with
regular labeling, and in fact we show that LTL model checking with respect
to pushdown systems with regular labeling is intereducible with LTL model
checking with respect to prefix-recognizable systems with simple
labeling. |
09:30- | 10:00
| Tatiana Rybina, U Manchester, UK Andrei
Voronkov, U Manchester, UK
**Using
canonical representations of solutions to speed up
infinite-state model checking**
In this paper we discuss reachability analysis for
infinite-state systems in which states can be represented by a vector of
integers. We propose a new algorithm for verifying reachability properties
based on canonical representations of solutions instead of decision
procedures for integer or real arithmetic. Experimental results demonstrate
that problems in protocol verification which are beyond the reach of other
existing systems can be solved completely automatically. |
10:00- | 10:30
| Walter Hartong, U Hannover, Germany Lars
Hedrich, U Hannover, Germany Erich
Barke, U Hannover, Germany
**On
discrete modeling and model checking for nonlinear analog
systems**
In this contribution we present a new method for developing
discrete models for nonlinear analog systems. Using an adaptive state space
intersection method the main nonlinear properties of the analog system can
be retained. Consequently, digital model checking ideas can be applied to
analog systems. To describe analog specification properties an extension to
the standard model checking language CTL and the appropriate, algorithmic
modifications are needed. Two nonlinear examples are given to show the
feasibility and the advantages of this method. |
*Chair:*
Joseph Sifakis
11:00- | 11:30
| Arindam Chakrabarti, U California-Berkeley, USA Luca
de Alfaro, U California-Santa Cruz, USA Thomas
A. Henzinger, U California-Berkeley, USA Freddy
Y. C. Mang, U California-Berkeley, USA
**Synchronous
and bidirectional component interfaces**
Component-based designs are typically conceived using an
"optimistic" approach: a component is designed under some assumptions about
its environment, with the expectation that the assumptions will be
satisfied in the complete design. In turn, the design may describe the
behavior of the component only when the component is in an environment that
satisfies the assumptions. We present interface models to capture this
approach to design. In these models, an interface describes both the input
assumptions of a component, and its output behavior. By enabling us to
check that the input assumptions of a component are met in a design,
interface models provide a basic kind of compatibility check for
component-based design. When refining a design into an implementation,
interface models require that the implementation behavior of a component
satisfies the design specification only when the input assumptions of the
component are satisfied, yielding greater flexibility in the choice of
implementations.
We present two interface models in detail, one for a
simple synchronous form of interaction between components typical in
hardware, and the other for more complex synchronous interactions on
bidirectional connections. As example for the latter, we specify the
interface of a bidirectional bus, with the input assumption that at any
time at most one component has write access to the bus. For these interface
models, we present algorithms for compatibility and refinement checking, as
well as efficient symbolic implementations. We also show how these
interface models lead to a rich methodology for the component-based design
and analysis of synchronous systems. |
11:30- | 12:00
| Arindam Chakrabarti, U California-Berkeley, USA Luca
de Alfaro, U California-Santa Cruz, USA Thomas
A. Henzinger, U California-Berkeley, USA Marcin
Jurdzinski, U California-Berkeley, USA Freddy
Y. C. Mang, U California-Berkeley, USA
**Interface
compatibility checking for software objects**
We present a formal methodology and tool for uncovering errors
in the interaction of software objects. Our methodology consists of a suite
of languages for defining object interfaces, and algorithms for checking
interface compatibility. An object interface makes assumptions about the
environment in the form of call and availability constraints. A call
constraint restricts the accessibility of local methods to certain external
methods. An availability constraint restricts the accessibility of local
methods to certain states of the object. For example, an interface for a
file server with local methods open and read may assert that a file cannot
be read without having been opened. Checking interface compatibility
requires the solution of games, and in the case of object interfaces with
availability constraints, of pushdown games. Using object interfaces, we
have uncovered incompatibilities in TinyOS, a small operating system for
sensor nodes in adhoc networks. |
12:00- | 12:30
| Michael A. Colón, Stanford U, USA Henny
B. Sipma, Stanford U, USA
**Practical
methods for proving program termination**
We present two algorithms to prove termination of programs by
synthesizing linear ranking functions. The first uses an invariant
generator based on iterative forward propagation with widening, and
extracts ranking functions from the generated invariants by manipulating
polyhedral cones. It is capable of finding subtle ranking functions which
are linear combinations of many program variables, but is limited to short
programs with few variables.
The second, more heuristic, algorithm
targets the class of structured programs with single-variable ranking
functions. Its invariant generator uses a heuristic extrapolation operator
to avoid iterative forward propagation over program loops. For the programs
we have considered, this approach converges faster and the invariants it
discovers are sufficiently strong to imply the existence of ranking
functions. |
*Chair:*
Gerard J. Holzmann
14:00- | 14:30
| Li Tan, State U of New York-Stony Brook, USA Rance
Cleaveland, State U of New York-Stony Brook, USA
**Evidence-based
model checking**
This paper shows that different "meta-model-checking" analyses can be
conducted
efficiently on a generic data structure we call a *support
set*. Support sets may be viewed as abstract encodings of the "evidence" a
model checker uses to
justify the yes/no answers it computes. We indicate how model checkers may
be modified to compute supports sets without compromising their time or
space complexity. We also show how support sets may be used for a variety
of different analyses of model-checking results, including: the generation
of diagnostic information for explaining negative model-checking results;
and certifying the results of model checking (is the evidence internally
consistent?). |
14:30- | 15:00
| Gianpiero Cabodi, Polytechnic of Turin, Italy Sergio
Nocco, Polytechnic of Turin, Italy Stefano
Quer, Polytechnic of Turin, Italy
**Mixing
forward and backward traversals in guided-prioritized
BDD-based verification**
Over the last decade BDD-based symbolic manipulations have been
among the most widely used core technologies in the verification domain and
various methodologies have been proposed to improve their efficiency.
Following some of the most successful trends proposed in this field, we
present in this paper a very promising approach to solve Unbounded Model
Checking problems.
Our approach is based on: Mixing forward and
backward traversals, dovetailing approximate and exact methods, adopting
guided and partitioned searches, efficiently using conjunctive
decompositions and generalized cofactor based BDD simplifications. A major
contribution of this paper is a backward verification procedure based on a
prioritized traversal, that we call "inbound-path-search". The method
consists in partitioning state sets in terms of the estimated distance from
the "target" set of states, and giving higher priority in the search
procedure to the subset with smallest estimated distance. An initial
approximate forward traversal produces over-approximated onion-ring
frontier sets that are used as distance estimators and guides for
prioritized backward traversal. The resulting method is exact and it does
not produce any false negatives.
We experimentally compare this
methodology with approximate-reachability don't cares in model checking, a
state-of-the-art BDD-based technique (implemented in the freely available
VIS tool) combining approximate and exact search. We show that we are able
to accomplish verification tasks outside its present scope. |
15:00- | 15:30
| Mitra Purandare, U Colorado-Boulder, USA Fabio
Somenzi, U Colorado-Boulder, USA
**Vacuum
cleaning CTL formulae**
Vacuity detection in model checking looks for properties that
hold in a model, and can be strengthened without causing them to fail. Such
properties often signal problems in the model, its environment, or the
properties themselves. The seminal paper of Beer et al. proposed an
efficient algorithm applicable to a restricted set of properties.
Subsequently, Kupferman and Vardi extended vacuity detection to more
expressive specification mechanisms. They advocated a more minute
examination of temporal logic formulae than the one adopted in [Beer97].
However, they did not address the issues of practicality and usefulness of
this more scrupulous inspection. In this paper we discuss efficient
algorithms for the detection of vacuous passes of temporal logic formulae,
showing that a thorough vacuity check for CTL formulae can be carried out
with very small overhead, and even, occasionally, in less time than plain
model checking. We also demonstrate the usefulness of such a careful
analysis with the help of case studies. |
*Chair:*
Natarajan Shankar
16:00- | 16:15
| Aaron Stump, Stanford U, USA Clark
W. Barrett, Stanford U, USA David
L. Dill, Stanford U, USA
**CVC:
a cooperating validity checker**
Decision procedures for decidable logics and logical theories
have proven to be useful tools in verification. This paper describes the
CVC ("a Cooperating Validity Checker") decision procedure. CVC implements a
framework for combining
subsidiary decision procedures for certain logical theories into a decision
procedure for the theories' union. Subsidiary decision procedures for
theories of arrays, inductive datatypes, and linear real arithmetic are
currently implemented. Other notable features of CVC are the incorporation
of the high-performance GRASP solver for propositional reasoning, and the
ability to produce independently checkable proofs for valid
formulas. |
16:15- | 16:30
| Marsha Chechik, U Toronto, Canada Benet
Devereux, U Toronto, Canada Arie
Gurfinkel, U Toronto, Canada
*ξ*Chek:
A multi-valued
model-checker
This paper describes a symbolic multi-valued model-checker
XChek. |
16:30- | 16:45
| Shoham Ben-David, IBM Haifa, Israel Anna
Gringauze, IBM Haifa, Israel Baruch
Sterin, IBM Haifa, Israel Yaron
Wolfsthal, IBM Haifa, Israel
**PathFinder:
A tool for design exploration**
In this paper we present a tool called PathFinder, which
exploits the power of model checking for developing and debugging
newly-written hardware designs. Our tool targets the community of design
engineers, who-in contrast to verification engineers-are not versed in
formal verification, and therefore have traditionally been distant from the
growing industry momentum in the area of model checking.
PathFinder
provides a means for the designer to explore, debug and gain insight into
the behaviors of the design at a very early stage of the
implementation-even before their design is complete. In the usage paradigm
enabled by PathFinder, which we call Design Exploration, the design
engineer specifies a behavior of interest, and the tool then finds and
demonstrates-graphically-a set of execution traces compliant with the
specified behavior, if any exist. When presented with each such execution
sequence, the designer is essentially furnished with an insight into the
design behavior, and specifically with an example of a concrete scenario in
which the behavior of interest occurs. This scenario can then be closely
inspected, refined, or abandoned in favor of another scenario. |
16:45- | 17:00
| Dennis Dams, Bell Labs, USA William
Hesse, U Massachusetts, USA Gerard
J. Holzmann, Bell Labs, USA
**Abstracting
C with abC**
A conceptually simple and practically very useful form of data
abstraction in model checking is variable hiding, which amounts to
suppressing all information about a given set of variables. The abC tool
automates this for programs written in the C programming language. It
features an integrated demand-driven pointer analysis, and has been
implemented as an extension of GCC. |
17:00- | 17:15
| Alex Groce, Carnegie Mellon U, USA Doron
A. Peled, U Texas-Austin, USA Mihalis
Yannakakis, Avaya Laboratories, USA
**AMC:
An adaptive model checker**
The AMC (for adaptive model checking) system allows one to
perform model checking directly on a system, even when its internal
structure is unknown or invisible. It also allows one to perform model
checking using an inaccurate model, incrementally improving the model each
time that a false negative (i.e., not an actual) counterexample is
found. |
*Room:*
Restaurant Luftkastellet
| |