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  
Piotr Hofman
Postdoctoral researcher, VERICONISS project 
Georg Zetzsche
Postdoctoral researcher, DAAD 

Ph.D. Students  
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 Ideal Theory for WSTS. In RP'16, LNCS 9899, pages 122. Springer, September 2016. ( BibTeX ) 
•  L. Beklemishev, S. Demri and A. Maté (eds.). Proceedings of the 11th Conference on Advances in Modal Logic (AiML'16), Budapest, Hungary, September 2016. College Publications. ( Web page  BibTeX ) 
•  P. A. Abdulla, S. Demri, A. Finkel, J. Leroux and I. Potapov (eds.). Selected papers of Reachability Problems Workshop 2012 (Bordeaux) and 2013 (Uppsala). Fundamenta Informaticae 143(34), 2016. ( Web page  BibTeX ) 
•  . On the Complexity of ResourceBounded Logics. In RP'16, LNCS 9899, pages 3650. Springer, September 2016. ( PDF  BibTeX ) 
•  . The height of piecewisetestable languages with applications in logical complexity. In CSL'16, Leibniz International Proceedings in Informatics 62, pages 37:137:22. LeibnizZentrum für Informatik, September 2016. ( PDF  BibTeX ) 