CAV on Wednesday

Detailed program
Wednesday July 31st, 2002
See also the unified by-slot program

All sessions take place in auditorium 1.

Session 17: Invited talk

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.

Session 18: Code Verification

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.

Session 19: Regular Model Checking

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

Session 20: Model 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).