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
Sylvain Schmitz
Assistant professor, ENS Cachan

Ph.D. Students

Nathan Grosshans
PhD student, Digiteo (joint with U. Montreal, Canada)
Anthony Lick
PhD student, ANR Prodaq
Simon Halfon
PhD student, ENS Cachan
Alessio Mansutti
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

N. Alechina, N. Bulling, S. Demri and B. LoganOn the Complexity of Resource-Bounded LogicsTheoretical Computer Science, 2018. Special issue of RP'16, to appear. PDF | BibTeX )
M. Blondin, A. Finkel and P. McKenzieWell Behaved Transition SystemsLogical Methods in Computer Science 13(3), pages 1-19, September 2017. Web page | BibTeX )
S. Demri, É. Lozes and A. MansuttiThe Effects of Adding Reachability Predicates in Propositional Separation LogicIn FoSSaCS'18, LNCS. Springer, April 2018. To appear. PDF | BibTeX )
S. SchmitzAlgorithmic Complexity of Well-Quasi-Orders.  Mémoire d'habilitation, École Normale Supérieure Paris-Saclay, France, November 2017. Web page | BibTeX )
M. Ganardi, D. König, M. Lohrey and G. ZetzscheKnapsack problems for wreath productsIn STACS'18, Leibniz International Proceedings in Informatics 96. Leibniz-Zentrum für Informatik, February 2018. To appear. Web page | BibTeX )

All the Infini publications