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)