 | |
All
sessions take place in auditorium 1.Chair:
Ed Brinksma | 09:00- | 10:00
| Gerard J. Holzmann, Bell Labs, USA
Invited
talk: Software analysis and model checking
Most
software developers today rely on only a small number of
techniques to check their code for defects: peer review, code
walkthroughts, and testing. Depsite a rrich literature on these subjects,
the results often leave much to be desired. The current software testing
process consumes a significant fraction of the overall resources in
industrial software development, yet it cannot promise zero-defect coed.
Tehre is reason to hope that the process can be improved. A range of tools
and techniques has become available in the last few years that can asses
the quality of code with considerably more rigor than before, and often
also with more easy. Many of the new tools can be understood as
applications of automata theory, and can readily be combined with logic
model checking techniques. |
| 10:00- | 10:30
| Thomas A. Henzinger, U California-Berkeley, USA
Ranjit
Jhala, U California-Berkeley, USA
Rupak
Majumdar, U California-Berkeley, USA
George
C. Necula, U California-Berkeley, USA
Grégoire
Sutre, LaBRI Bordeaux, France
Westley
Weimer, U California-Berkeley, USA
Temporal-safety
proofs for systems code
We present a methodology and tool for verifying and certifying
systems code. The verification is based on the lazy-abstraction paradigm
for intertwining the following three logical steps: construct a predicate
abstraction from the code, model check the abstraction, and automatically
refine the abstraction based on counterexample analysis. The certification
is based on the proof-carrying code paradigm. Lazy abstraction enables the
automatic construction of small proof certificates. The methodology is
implemented in Blast, the Berkeley Lazy Abstraction Software Verification
Tool. We describe our experience applying Blast to Linux and Windows device
drivers and we describe how error traces are produced for erroneous drivers
and easily checkable correctness certificates are produced for the correct
drivers. |
Chair:
Amir Pnueli | 11:00- | 11:30
| Ahmed Bouajjani, U Paris VII, France
Tayssir
Touili, U Paris VII, France
Extrapolating
tree transformations
We consider the framework of regular tree model
checking where sets of configurations of a system are represented by
regular tree languages and its dynamics is modeled by a term rewriting
system (or a regular tree transducer). We focus on the computation of the
reachability set R*(L) where R is a regular tree
transducer and L is a regular tree language. The construction of this
set is
not possible in general. Therefore, we present a general acceleration
technique, called regular tree widening which allows to
speed up the convergence of iterative fixpoint computations in regular tree
model checking. This technique can be applied uniformly to various kinds of
transformations.
We show the application of our framework to different
analysis contexts: verification of parametrized tree networks and data-flow
analysis of multithreaded programs. Parametrized networks are modeled by
relabeling tree transducers, and multithreaded programs are modeled by term
rewriting rules encoding transformations on control structures.
We
prove that our widening technique can emulate many existing algorithms for
special classes of transformations and we show that it can deal with
transformations beyond the scope of these algorithms. |
| 11:30- | 12:00
| Parosh Aziz Abdulla, Uppsala U, Sweden
Bengt
Jonsson, Uppsala U, Sweden
Pritha
Mahata, Uppsala U, Sweden
Julien
d'Orso, Uppsala U, Sweden
Regular
tree model checking
In this paper, we present an approach for algorithmic
verification of infinite-state systems with a parameterized tree topology.
Our work is a generalization of regular model checking, where we extend the
work done with strings toward trees. States are represented by trees over a
finite alphabet, and transition relations by regular, structure preserving
relations on trees. We use an automata theoretic method to compute the
transitive closure of such a transition relation. Although the method is
incomplete, we present sufficient conditions to ensure termination.
We
have implemented a prototype for our algorithm and show the result of its
application on a number of examples. |
| 12:00- | 12:30
| Robert Kurshan, Cadence Design Systems, USA
Vladimir
Levin, Bell Labs, USA
Husnu
Yenigun, Sebancy U, Turkey
Compressing
transitions for model checking
An optimization technique is presented that compresses a chain
of transitions into a single jump transition, thus making a model smaller
prior to model checking. We give compression algorithms, together with
conditions that allow such compressions to preserve next-time-free LTL.
Experimental results are presented and discussed.
Keywords: model
checking, partial order reduction |
Chair:
Kim Guldstrand Larsen | 14:00- | 14:30
| Victor Khomenko, U Newcastle upon Tyne, UK
Maciej
Koutny, U Newcastle upon Tyne, UK
Walter
Vogler, U Augsburg, Germany
Canonical
prefixes of Petri net unfoldings
In this paper, we develop a general technique for truncating
Petri net unfoldings, parameterized according to the level of information
about the original unfolding one wants to preserve. Moreover, we propose a
new notion of completeness of a truncated unfolding. A key aspect of our
approach is an algorithm-independent notion of cut-off events, used to
truncate a Petri net unfolding. Such a notion is based on a cutting context
and results in the unique canonical prefix of the unfolding. Canonical
prefixes are complete in the new, stronger sense, and we provide necessary
and sufficient conditions for its finiteness, as well as upper bounds on
its size in certain cases. A surprising result is that after suitable
generalization, the standard unfolding algorithm presented in [Esparza,
Roemer and Vogler: An Improvement of McMillan's Unfolding Algorithm. Proc.
TACAS'96] and the parallel unfolding algorithm proposed in [Heljanko,
Khomenko and Koutny: Parallelisation of the Petri Net Unfolding Algorithm.
Proc. of TACAS'02], despite being non-deterministic, generate the canonical
prefix. This gives an alternative correctness proof for the former
algorithm, and a new (much simpler) proof for the latter one. |
| 14:30- | 15:00
| Stefan Blom, CWI Amsterdam, The Netherlands
Jaco
van de Pol, CWI Amsterdam, The Netherlands
State
space reduction by proving confluence
We present a modular method for on-the-fly state space
reduction. The theoretical foundation of the method is a new confluence
notion for labeled transitions systems. The method works by adding
confluence information to the symbolic representation of the state space.
We present algorithms for on-the-fly exploration of the reduced state
space, for generating confluence information and for a symbolic reduction,
called prioritization. The latter two algorithms rely on an automated
theorem prover to derive the necessary information. We also present some
case studies in which tools that implement these algorithms were
used. |
| 15:00- | 15:30
| Sankar Gurumurthy, U Colorado-Boulder, USA
Roderick
Bloem, Graz U of Techn., Austria
Fabio
Somenzi, U Colorado-Boulder, USA
Fair
simulation minimization
We present an algorithm for the minimization of Buechi automata
based on the notion of fair simulation introduced in
[HKR97]. Unlike direct simulation, fair simulation allows flexibility in
the satisfaction of the acceptance conditions, and hence leads to larger
relations. However, it is not always possible to remove edges to simulated
states or merge simulation equivalent states without altering the language
of the automaton. Solutions proposed in the past consisted in checking
sufficient conditions [SB00, Theorem 3], or resorting to more restrictive
notions like delayed simulation [EWS01]. By contrast, our algorithm
exploits the full power of fair simulation by efficiently checking the
correctness of changes to the automaton (both mergers of states and removal
of edges). |
| |
![[previous]](../img/prev.gif){kind=small}
![[up]](../img/up.gif){kind=small}
![[next]](../img/next.gif){kind=small}
