DYNAMO 2nd meeting, Thursday 27 May, Grenoble
---------------------------------------------

9h00 - 9h30	 breakfast

9h30 - 10h30	 Peter Habermehl: Abstract Regular Model Checking.

We propose abstract regular model checking as a new generic technique
for verification of parametric and infinite-state systems. The technique
combines the two approaches of regular model checking and verification
by abstraction. We propose a general framework of the method as well as
several concrete ways of abstracting automata or transducers, which we
use for modelling systems and encoding sets of their configurations as
usual in regular model checking. The abstraction is based on collapsing
states of automata (or transducers) and its precision is being incrementally
adjusted by analysing spurious counterexamples. We illustrate the technique
on verification of a wide range of systems including a novel application
of automata-based techniques to an example of systems with dynamic linked
data structures.

(joint work with Peter Habermehl and Tomas Vojnar)

10h30 - 11h30	 Ahmed Bouajjani: Handling Liveness Properties in (omega-)Regular Model Checking.

(joint work with Axel Legay and Pierre Wolper)

11h30 - 12h30	  Marius Bozga: Concurrency of Operations on BTrees - A Case Study Proposal

We investigate three published algorithms for concurrent access to dynamic
tree structures, usually implemented by datavase systems. This analysis
points to some properties that need to be considered by a future verification
method which is intended for programs that combine concurrency and dynamic
memory structures.

(joint work with Radu Iosif)