DYNAMO meeting #5, Monday, 26/06/2006, Grande salle de Verimag
==============================================================
* 10h00 Coffee
* 10h30 - Tayssir Touili (Liafa, Paris): Verifying Concurrent Message-Passing C Programs with Recursive Calls
We consider the model-checking problem for C programs with (1) data
ranging over very large domains, (2) (recursive) procedure calls,
and (3) concurrent parallel components that communicate via
synchronizing actions. We model such programs using communicating
pushdown systems, and reduce the reachability problem for this model
to deciding the emptiness of the intersection of two context-free
languages L1 and L2. We tackle this undecidable problem using a
CounterExample Guided Abstraction Refinement (CEGAR) scheme. We
implemented our technique in the model checker MAGIC and found a
previously unknown bug in a version of a Windows NT Bluetooth driver.
* 11h15 - Marius Bozga (Verimag, Grenoble): Deciding Safety and Termination Properties for Flat Programs with Lists
In this paper we analyze the complexity of checking safety and termination properties,
for a very simple, yet non-trivial, class of programs with singly-linked list data structures.
Since, in general, programs with lists are known to have the power of Turing machines, we restrict
the control structure, by forbidding nested loops and destructive updates. Surprisingly, even with
these simplifying conditions, programs working on heaps with more than one cycle are undecidable,
whereas decidability can be established when the input heap may have at most one loop. The proofs
for both the undecidability and the decidability results rely on non-trivial number-theoretic results.
* 12h00 Lunch
* 13h30 - Ahmed Bouajjani (Liafa, Paris): Reasoning about dynamic networks of infinite-state processes
We introduce new models for multithreaded programs with dynamic creation of communicating processes, each of these processes
being able to manipulate a finite number of (local) variables over infinite data domains. These models are based on constrained
multiset rewrite systems (Petri nets). We define a logic allowing to specify and to reason about (potentially infinite) sets of
configurations of such models. We investigate the decidability of the proposed logic and propose an expressive fragment which is
decidable and close under post and pre image computations. We show the application of the proposed framework in the verification
of parametrized/dynamic networks of processes with integer, real, or stack variables. This is a joint work with Yan Jurski and Mihaela Sighireanu.
* 14h30 - Guillaume Salagnac (Verimag, Grenoble): Efficient Region-Based Memory Management for Resource-limited Real- Time Embedded Systems
This paper presents a simple and efficient static analysis
algorithm, combined with a region allocation policy for real-time
embedded Java applications. The goal of this work is to provide a
static analysis mechanism efficient enough to be integrated in an
assisted-development environment, and to implement region-based
memory management primitives suited for resource-limited platforms
such as smart cards.
* 15h30 - 16h00 Coffee
* 16h00 - Peter Habermehl (Liafa, Paris): Abstract Tree Regular Model Checking of Complex Dynamic Data Structures
We consider the verification of non-recursive C programs
manipulating dynamic linked data structures with possibly
several next pointer selectors and with finite domain
non-pointer data. We aim at checking basic memory consistency
properties (no null pointer assignments, etc.) and shape invariants
whose violation can be expressed in an existential fragment of a
first order logic over graphs. We formalise this fragment as a logic
for specifying bad memory patterns whose formulae may be translated
to testers written in C that can be attached to the program, thus
reducing the verification problem considered to checking
reachability of an error control line. We encode configurations of
programs, which are essentially shape graphs, in an original way as
extended tree automata and we represent program statements by tree
transducers. Then, we use the abstract regular tree model checking
framework for a fully automated verification. The method has been
implemented and successfully applied on several case studies.
* 16h40 Radu Iosif (Verimag, Grenoble): Extending Separation Logic for Quantitative Reasoning
*** Work in progress ***
We present an extension of the decidable fragment of
Separation Logic for singly-linked lists, previously introduced
by Berdine, Calcagno and O'Hearn. The main extension consists in
introducing atomic formulae of the form $ls^k(x, y)$ describing a
list segment of length $k$, stretching from $x$ to $y$, and allowing
the integer variables $k$ to occur further within Presburger formulae.
We study the decidability properties of the full first-order logic
combining unrestricted quantification of arithmetic and location
variables. Although the full logic is found to be undecidable,
formulae with the quantifier prefix in the language
$\exists^* \{\exists_\nat, \forall_\nat\}^*$ are decidable.
We provide here two arguments for decidability of entailments
in this logic, corresponding to two different approaches for the satisfiability
problem: (1) a small model theorem and (2) an automata-theoretic method.
* 17h00 - Closing discussions
* 20h00 - Farewell dinner (TBA)