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