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 
Stefan Göller
Researcher, CNRS 
Philippe Schnoebelen
Senior researcher, CNRS 
Alain Finkel
Professor, ENS Cachan 
Étienne Lozes
Assistant professor, ENS Cachan 

Associated and Temporary Members  
Christoph Haase
Postdoctoral researcher, VERICONISS project 
Piotr Hofman
Postdoctoral researcher, VERICONISS project 
Georg Zetzsche
Postdoctoral researcher, DAAD 
Ph.D. Students  
Michael Blondin
PhD student, Digiteo (joint with U. Montreal, Canada) 
Simon Halfon
PhD student, ENS Cachan 
The main thrust for our investigations revolves around the decidability, algorithmics and complexity of wellstructured transition systems (WSTS) and of the most commonly used wellquasiorders (wqo). Let us just mention three kinds of projects (involving WSTS/wqo) among all others:
One of the most useful decidable problems on WSTS for verification is coverability, because it allows to check safety properties. This is decidable thanks to a now classical backward algorithm, that attempts to reach the initial configuration backwards from the set of states that cover the target configuration. Nevertheless, forward procedures are felt to be more efficient than backward procedures in general: e.g., for lossy channel systems, although the backward procedure always terminates, only a (necessarily nonterminating) forward procedure is implemented in the TREX tool. We have derived similar generic algorithms that proceed forward. This work draws from topological generalizations of wqos, and comprises two main contributions: wqo completions and complete WSTS.
The theory of complete wqos and complete WSTS currently deals mostly with decidability and/or forward analysis. This field is still mostly uncovered (e.g., good datastructures for ideals have only been proposed for the two simplest wqos used in verification). We intend to pursue this topic by exploring in more depth the possibilities that have been opened: complexity and generic datastructures for completionbased algorithms (i.e., for ideals, cones, limits), coverability trees and graphs for complete WSTS.
Completion techniques (and new wellstructured systems) open the way to regular modelchecking approaches for the verification of new models. For some of them, for instance for priority channel systems, we intend to develop datastructures, acceleration techniques, and finally prototypes, tools demonstrating the feasibility of automated verification.
Except in a few pioneering works, the computational costs of WSTSbased methods has not really been analyzed or even addressed until recently. The explanation behind this omission is that we were lacking concepts and results on the complexity of the most commonly used wqos, beginning with tuples of natural numbers and words ordered by embedding. This issue goes beyond WSTS and verification.
In the last five years, we developed a theoretical framework that allows to measure the complexity of algorithms (and problems) involving these wqos:
•  . The height of piecewisetestable languages with applications to logical complexity. In CSL'16, Leibniz International Proceedings in Informatics. LeibnizZentrum für Informatik, September 2016. To appear. ( BibTeX ) 
•  . On the Parallel Complexity of Bisimulation over Finite Systems. In CSL'16, Leibniz International Proceedings in Informatics. LeibnizZentrum für Informatik, September 2016. To appear. ( BibTeX ) 
•  . The complexity of downward closure comparisons. In ICALP'16, Leibniz International Proceedings in Informatics. LeibnizZentrum für Informatik, July 2016. To appear. ( PDF  BibTeX ) 
•  . Deciding Piecewise Testable Separability for Regular Tree Languages. In ICALP'16, Leibniz International Proceedings in Informatics. LeibnizZentrum für Informatik, July 2016. To appear. ( Web page  BibTeX ) 
•  . A PolynomialTime Algorithm for Reachability in Branching VASS in Dimension One. In ICALP'16, Leibniz International Proceedings in Informatics. LeibnizZentrum für Informatik, July 2016. To appear. ( Web page  BibTeX ) 