LIAFA, 175 rue du Chevaleret Paris 13eme

9h00 Coffee

9h15 Tayssir Touili (LIAFA) :

An Expressive Framework for State/Event Systems

Abstract:

Specification languages for concurrent software systems need to

combine practical algorithmic efficiency with high expressive power

and the ability to reason about both states and events. We address

this question by defining a new branching-time temporal logic

which integrates both state-based and action-based

properties. This logic is universal, i.e., preserved by the simulation

relation, and thus amenable to counterexample-guided abstraction

refinement. We provide a model-checking algorithm for this logic, and

describe a compositional abstraction-refinement loop which exploits

the natural decomposition of the concurrent system; the abstraction

and refinement steps are performed over each component separately, and

only the model checking step requires an explicit composition of the

abstracted components. For experimental evaluation, we have

integrated the presented algorithms in the software verification tool

MAGIC, and determined a previously unknown race condition error in a

piece of an industrial robot control software.

10h00 Pause

10h15 Peter Habermehl (LIAFA):

Verifying Programs with 1-Selector-Linked Structures in Regular Model Checking

Abstract:

We address the problem of automatic verification of programs with dynamic data structures. We consider the case of sequential, non-recursive programs manipulating 1-selector-linked structures such as traditional linked lists (possibly sharing their tails) and circular lists. We propose an automata-based approach for a symbolic verification of such programs using the regular model checking framework. Given a program, the configurations of the memory aresystematically encoded as words over a suitable finite alphabet, potentially infinite sets of configurations are represented by finite-state automata, and statements of the program are automatically translated into finite-state transducers defining regular relations between configurations. Then, abstract regular model checking techniques are applied in order to automatically check safety properties concerning the shape of the computed configurations or relating the input and output configurations. For this particular purpose, we introduce new techniques for the computation of abstractions of the set of reachable configurations and to refine these abstractions if spurious counterexamples are detected. Finally, we present experimental results showing the applicability of the approach and its efficiency.

acceleration problem for integer counter automata.

11h00 Pause

11h15 Radu Iosif (VERIMAG):

"Quantitative Verification of Programs with Lists"

In this work we study imperative programs that handle list objects, performing unrestricted selector updating operations. For this class of programs, we address the problem of {\em quantitative verification}, by reasoning about arithmetic relations between the lengths of certain lists. We first show undecidability of the general problem, by reduction from the reachability problem for two-counter machines. Second, we introduce a decidable property specification logic and we study the complexity of the decision problem. Finally, we propose a semi-algorithmic method for the verification of Hoare-Floyd style properties of programs with lists. Using this method, we can reduce the invariant computation problem for a program with lists to an acceleration problem for integer counter automata.

12h00 Pause

13h30 Julien D'Orso (LIAFA):

Simulation-Based Iteration of Tree Transducers

Abstract:

Regular model checking is the name of a family of techniques for

analyzing infinite-state systems in which states are represented by

words, sets of states by finite automata, and transitions by

finite-state transducers. The central problem is to

compute the transitive closure of a transducer. A main obstacle

is that the set of reachable states is in general not regular.

Recently, regular model checking has

been extended to systems with tree-like architectures.

In this paper, we provide a procedure, based on a new implementable acceleration technique, for computing the transitive closure of a tree transducer. The procedure consists of incrementally adding new transitions while merging states which are related according to a pre-defined equivalence relation. The equivalence is induced by a {\it downward} and an {\it upward} simulation relation which can be efficiently computed. Our technique can also be used to compute the

set of reachable states without computing the transitive closure. We

have implemented and applied our technique to several protocols.

14h15 Guillaume Salagnac (VERIMAG):

"Fast escape analysis for region-based memory management"

Abstract: We present an algorithm for escape analysis inspired by, but

more precise than, the one proposed by Gay and Steensgaard. The

primary purpose of our algorithm is to produce useful information to

allocate objects using a region-based memory manager. The algorithm

combines intraprocedural variable-based and interprocedural points-to

analyses. This is a work in progress towards achieving an

application-oriented trade-off between precision and scalability. We

illustrate the algorithm on several typical programming patterns, and

show experimental results of a first prototype on a few benchmarks.

15h00 Discussion