Presentation of Infini
The INFINI axis focuses on verifying infinite systems: programs that manipulate unbounded values, recursive communicating processes, parametrized systems. In this context, our purpose is to identify classes of models and properties for which automated verification is possible.
Permanent Members | ||
|
Stéphane Demri
Senior researcher, CNRS |
Sylvain Schmitz
Assistant professor, ENS Paris-Saclay |
|
|
Alain Finkel
Professor, ENS Paris-Saclay |
Philippe Schnoebelen
Senior researcher, CNRS |
|
Associated Members | ||
|
Simon Halfon
ATER, ENS Paris-Saclay |
||
Ph.D. Students | ||
|
Anthony Lick
PhD student, ANR Prodaq |
Alessio Mansutti
PhD student, ENS Paris-Saclay |
|
We study algorithmic aspects of infinite-state systems. A particular focus has been on the class of well-structured transition systems (WSTS), vector addition systems, heap-manipulating systems and lifo-like infinite-state systems. Let us just mention four kinds of projects in these areas
A classical principle in WSTS is to reduce the problem at hand to the computation of ascending chain of upward-closed sets. The underlying well-quasi order (wqo) guarantees that the chain eventually stabilises and each set of the chain can be finitely presented as the upward-closure of finitely many elements. We are currently investigating the algorithmics of downward-closed for which descending chains are also finite. In particular we are study the algorithmic manipulation of downward-closed set in wqo's in terms of finite unions of ideals, which can be seen as downward-closed sets that are irreducible. LOYD This line of research has applicaitons in studying generalisations of WSTS, provide solutions to problems in formal languages theory, yield new techniques for complexity upper bounds for WSTS and give new insights on classical algorithms solving reachability in vector addition systems, just to mention a few. .
Vector addition systems (VAS) form a particular class of well-structured transitions systems running over a finite set of counters. A central problem is the reachability problem. Indeed, a plethora of problems in computer science reduce to VAS reachability, as for instance the satisfiability problem for expressive data logics. We currently study extensions of VAS. A particular focus lies in the study of branching VAS which extends VAS by allowing the counters to be split, thus allowing to model the sharing of ressources but more importantly having applications in various fields like computation linguistics and linear logic but also to logics on XML trees.
We are interested in the analysis of pointer-manipulating programs, which can be seen as a particular class of infinite- state systems. Separation logic is known as an assertion language to perform verification, by extending Hoare-Floyd logic in order to verify programs with mutable data structures. We are studying the decidability and complexity of various fragments of separation logic. So far we have studied the role of first-order quantifiers in the undecidability of plain separation logic, i.e. with points-to predicate, all Boolean connectives and magic wand, but without recursive predicates and more advanced constructs. Our agenda is focused on the development of decision procedures for separation logics with inductive definitions (to describe shapes such as lists, trees or user-defined recursive structures) and with quantitative properties about the memory cells such as data values or access permissions. In particular, being able to tame fragments of separation logics with the magic wand is one of our major goals.
Another important class of infinite-state systems in the focus of our research are LIFO-like infinite state systems, i.e. finite-state machines that can manipulate an unbounded data structure in a last-in first-out fashion -- thus faithfully allowing to model recursion in computer programs. We study elementary questions like the reachability problem on such models, but also investigate the computational complexity of deciding the behavioral equivalence between such systems.