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 ParisSaclay 

Alain Finkel
Professor, ENS ParisSaclay 
Philippe Schnoebelen
Senior researcher, CNRS 

Associated Members  
Simon Halfon
ATER, ENS ParisSaclay 

Ph.D. Students  
Anthony Lick
PhD student, ANR Prodaq 
Alessio Mansutti
PhD student, ENS ParisSaclay 
We study algorithmic aspects of infinitestate systems. A particular focus has been on the class of wellstructured transition systems (WSTS), vector addition systems, heapmanipulating systems and lifolike infinitestate 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 upwardclosed sets. The underlying wellquasi order (wqo) guarantees that the chain eventually stabilises and each set of the chain can be finitely presented as the upwardclosure of finitely many elements. We are currently investigating the algorithmics of downwardclosed for which descending chains are also finite. In particular we are study the algorithmic manipulation of downwardclosed set in wqo's in terms of finite unions of ideals, which can be seen as downwardclosed 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 wellstructured 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 pointermanipulating 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 HoareFloyd 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 firstorder quantifiers in the undecidability of plain separation logic, i.e. with pointsto 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 userdefined 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 infinitestate systems in the focus of our research are LIFOlike infinite state systems, i.e. finitestate machines that can manipulate an unbounded data structure in a lastin firstout 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.