INFINI: Algorithms for Symbolic Verification

Research Topics

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
Post-doctoral 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 well-structured transition systems (WSTS) and of the most commonly used well-quasi-orders (wqo). Let us just mention three kinds of projects (involving WSTS/wqo) among all others:

Algorithmics of Complete WSTS/WQOs

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 non-terminating) 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 data-structures 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 data-structures for completion-based algorithms (i.e., for ideals, cones, limits), coverability trees and graphs for complete WSTS.

Regular Model-Checking and Complete WSTS

Completion techniques (and new well-structured systems) open the way to regular model-checking approaches for the verification of new models. For some of them, for instance for priority channel systems, we intend to develop data-structures, acceleration techniques, and finally prototypes, tools demonstrating the feasibility of automated verification.

Algorithmic Theory of WQOs

Except in a few pioneering works, the computational costs of WSTS-based 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:

  • Complexity upper bounds are obtained by careful computations in the ordinal-recursive hierarchies first considered in Recursion theory and in Proof Theory. We managed to provide upper bounds for several classical WSTSs; in particular lossy channel systems and monotonic counter machines, and for some richer systems like timed-arc nets.
  • Establishing complexity lower bounds requires new reduction techniques. Following on our early success with lossy channel systems, we developed coding techniques for simulating ordinal-recursive computations in WSTSs in a robust way, i.e., with encodings that are compatible with the wqo. The versatility of these techniques is high and we could use them to prove very high lower bounds for a variety of systems: reset nets, lossy channels, timed-arc nets, priority channels, etc.


Current Projects

Past Projects

About LSV

Presentation of Infini (2013)

Infini presentation at AERES (2013)

Recent Publications

All the Infini publications

F. Bruse, N. Kobayashi and É. LozesOn the Relationship Between Higher-Order Recursion Schemes and Higher-Order Fixpoint LogicIn POPL'17. ACM Press, January 2017. To appear. BibTeX )
S. Demri, V. Goranko and M. LangeTemporal Logics in Computer Science, Cambridge Tracts in Theoretical Computer Science 58. Cambridge University Press, October 2016. Web page | BibTeX )
M. Hutagalung, N. Hundeshagen, D. Kuske, M. Lange and É. LozesMulti-Buffer Simulations for Trace Language InclusionIn GandALF'16, Electronic Proceedings in Theoretical Computer Science 226, pages 213-227. September 2016. PDF | BibTeX )
M. Hutagalung, N. Hundeshagen, D. Kuske, M. Lange and É. LozesTwo-Buffer Simulation GamesIn Cassting/SYNCOP'16, Electronic Proceedings in Theoretical Computer Science 220, pages 213-227. April 2016. PDF | BibTeX )
É. LozesA Type-Directed Negation EliminationIn FICS'15, Electronic Proceedings in Theoretical Computer Science 191, pages 132-142. September 2015. PDF | BibTeX )

All the Infini publications