VERIDYC Meeting, 16/02/2012, CTL Amphi
10h-10h30 Coffee, croissants
10h30-11h15 Constantin Enea (LIAFA) Accurate Invariant Checking for List-Manipulating Programs with Infinite Data
We propose a logic-based framework for automated reasoning about
sequential programs manipulating singly-linked lists with unbounded
data. We introduce the logic SLD, which allows to combine shape
constraints, written in a fragment of Separation Logic, with data and
size constraints. We address the problem of checking the entailment
between SLD formulas, which is crucial in performing pre-post
condition reasoning. Although this problem is undecidable in general
for SLD, we propose a sound and powerful procedure that is able to
solve this problem for a large class of formulas, beyond the
capabilities of existing techniques and tools. Moreover, we prove that
this procedure is complete, i.e., it is actually a decision procedure
for this problem, for an important fragment of SLD including known
decidable logics. We have implemented this procedure and shown its
preciseness and its efficiency on a significant benchmark of
formulas. This is a joint work with Ahmed Bouajjani, Cezara Dragoi,
and Mihaela Sighireanu.
11h15-12h00 Ahmed Bouajjani (LIAFA) Analysis of recursively parallel programs
We propose a general formal model of isolated hierarchical parallel
computations, and identify several fragments to match the concurrency
constructs present in real-world programming languages such as Cilk
and X10. By associating fundamental formal models (vector addition
systems with recursive transitions) to each fragment, we provide a
common platform for exposing the relative difficulties of algorithmic
reasoning. For each case we measure the complexity of deciding
state-reachability for finite-data recursive programs, and propose
algorithms for the decidable cases. The complexities which include
PTIME, NP, EXPSPACE, and 2EXPTIME contrast with undecidable
state-reachability for recursive multi-threaded programs. [This is a
joint work with Michael Emmi]
12h00-13h30 Lunch + coffee (on site)
13h30-14h15 Peter Habermehl (LIAFA) Forest Automata for Verification of Heap Manipulation
We consider verification of programs manipulating dynamic linked data
structures such as various forms of singly and doubly-linked lists or
trees. We consider important properties for this kind of systems like
no null-pointer dereferences, absence of garbage, shape properties,
etc. We develop a verification method based on a novel use of tree
automata to represent heap configurations. A heap is split into
several ``separated'' parts such that each of them can be represented
by a tree automaton. The automata can refer to each other allowing the
different parts of the heaps to mutually refer to their
boundaries. Moreover, we allow for a hierarchical representation of
heaps by allowing alphabets of the tree automata to contain other,
nested tree automata. Program instructions can be easily encoded as
operations on our representation structure. This allows verification
of programs based on a symbolic state-space exploration together with
refinable abstraction within the so-called abstract regular tree model
checking. A motivation for the approach is to combine advantages of
automata-based approaches (higher generality and flexibility of the
abstraction) with some advantages of separation-logic-based approaches
(efficiency). We have implemented our approach and tested it
successfully on multiple non-trivial case studies. (joint work with
Lukas Holik, Adam Rogalewicz, Jiri Simacek and Tomas Vojnar)
14h15-15h00 Radu Iosif (VERIMAG) Deciding Conditional Termination
This paper addresses the problem of conditional termination, which is
that of defining the set of initial configurations from which a given
program terminates. First we define the dual set, of initial
configurations, from which a non-terminating execution exists, as the
greatest fixpoint of the pre-image of the transition relation. This
definition enables the representation of this set, whenever the closed
form of the relation of the loop is definable in a logic that has
quantifier elimination. This entails the decidability of the
termination problem for such loops. Second, we present effective ways
to compute the weakest precondition for non-termination for difference
bounds and octagonal (non-deterministic) relations, by avoiding
complex quantifier eliminations. We also investigate the existence of
linear ranking functions for such loops. Finally, we study the class
of linear affine relations and give a method of under-approximating
the termination precondition for a non-trivial subclass of affine
relations. We have performed preliminary experiments on transition
systems modeling real-life systems, and have obtained encouraging
results. Joint work with Marius Bozga and Filip Konecny
15h00-15h45 David Monniaux (VERIMAG) Distinguishing paths (for fun and profit)
Usual techniques in abstract interpretation apply "join" operations
when control flows from several nodes. Unfortunately, these techniques
introduce imprecision, resulting in not being able to prove desired
properties. Modern SMT-solving techniques allow enumerating paths "on
demand". We shall see how such path techniques may be combined with
conventional polyhedral analysis, quantifier elimination, or with
policy iteration, in order to obtain more precise invariants. Joint
work with Thomas Gawlitza, Laure Gonnord and Julien Henry
15h45-16h15 Coffee break
16h15-17h15 C Front End Session
* Etienne Lozes : The Cheap plugin
* Florent Garnier : The Flata-C plugin
* Julien Henry : TBA
20h00 Bombay