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  
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:
•  . On the Relationship Between HigherOrder Recursion Schemes and HigherOrder Fixpoint Logic. In POPL'17. ACM Press, January 2017. To appear. ( BibTeX ) 
•  . Temporal Logics in Computer Science, Cambridge Tracts in Theoretical Computer Science 58. Cambridge University Press, October 2016. ( Web page  BibTeX ) 
•  . MultiBuffer Simulations for Trace Language Inclusion. In GandALF'16, Electronic Proceedings in Theoretical Computer Science 226, pages 213227. September 2016. ( PDF  BibTeX ) 
•  . TwoBuffer Simulation Games. In Cassting/SYNCOP'16, Electronic Proceedings in Theoretical Computer Science 220, pages 213227. April 2016. ( PDF  BibTeX ) 
•  . A TypeDirected Negation Elimination. In FICS'15, Electronic Proceedings in Theoretical Computer Science 191, pages 132142. September 2015. ( PDF  BibTeX ) 