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.

Members

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
Post-doctoral researcher, VERICONISS project
Georg Zetzsche
Post-doctoral researcher, DAAD
 

Ph.D. Students

Simon Halfon
PhD student, ENS Cachan
 

Presentation

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.

Funding

Current Projects

Past Projects

About LSV

Presentation of Infini (2013)

Infini presentation at AERES (2013)

Recent Publications

All the Infini publications

A. FinkelThe Ideal Theory for WSTSIn RP'16, LNCS 9899, pages 1-22. 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(3-4), 2016. Web page | BibTeX )
N. Alechina, N. Bulling, S. Demri and B. LoganOn the Complexity of Resource-Bounded LogicsIn RP'16, LNCS 9899, pages 36-50. Springer, September 2016. PDF | BibTeX )
P. Karandikar and Ph. SchnoebelenThe height of piecewise-testable languages with applications in logical complexityIn CSL'16, Leibniz International Proceedings in Informatics 62, pages 37:1-37:22. Leibniz-Zentrum für Informatik, September 2016. PDF | BibTeX )

All the Infini publications