ACI DYNAMO
					==========

					VERIMAG, Grenoble
					28 November 2003


9:30 - 10:00		Breakfast

10:00 - 11:00		Ahmed Bouajjani 
-------------------------------------------------------------------------------
TITLE: Automata-theoretic techniques for the analysis of 
multithreaded programs with procedure calls.

ABSTRACT:
We consider the verification problem of programs with unbounded
(1) recursive procedure calls, and
(2) dynamic creation of concurrent processes.

Programs are modeled using term rewrite systems called PRS
(for process rewrite systems).
These models are more powerful than pushdown automata and Petri nets,
two common models for reasoning about, respectively,
recursive programs without process creation,
and multi-threaded programs without recursive calls.

We present various techniques for symbolic reachability analysis
of these models using different tree automata-based representation structures

for sets of configurations.
Our results generalize and unify existing results for the analysis
of subclasses of PRS. In particular, we provide a construction
allowing to integrate analysis procedures for pushdown automata
with procedures for the (exact/approximate) analysis of Petri nets
in order to analyze PRS systems.

This a joint work with Tayssir Touili.
-------------------------------------------------------------------------------

11:00 - 12:00	  Radu Iosif
-------------------------------------------------------------------------------
TITLE: An Effective Calculus for the Verification of Aliasing Properties

ABSTRACT:
In this work we develop a deductive verification method 
based on a logic that describes pointer aliasing. 
The user has to annotate the program with loop invariants, 
pre- and post-conditions. The annotations are then automatically 
checked for validity by computing weakest preconditions in our
effectively decidable logic. We start by discussing the undecidability
of a very expressive program logic (wAL), then define a decidable 
subset (pAL) that is closed under the weakest precondition operators. 
For the latter logic we give two sound and complete proof systems,
one based on natural deduction system, and another based on the
effective method of analytic tableaux.

This is joint work with Marius Bozga and Yassine Lakhnech
-------------------------------------------------------------------------------

12:00 - 14:00	 Lunch

14:00 - 15:00	 Sergio Yovine
-------------------------------------------------------------------------------
TITLE: On synthesizing parametric specifications of dynamic memory 
utilization

ABSTRACT:
We present a static analysis approach for estimating the
amount of memory dynamically allocated by a piece of code. The technique
is suitable for languages with high-level memory management mechanisms
like Java and resorts to ideas that come from the community of
parallel computing and the field of pointer escape analysis.
Firstly, we propose a general procedure for synthesizing a parametric
specification which over-estimates the amount of memory allocated by a
program method in terms of its parameters. Then, we introduce a series
of extensions to deal with the problem of estimating memory consumption
in a scoped-memory management setting.

(joint work with Victor Braberman and Diego Garbervetsky)
-------------------------------------------------------------------------------

15:00 - 16:00	Technical Discussions

16:00 - 17:00	Organization Details