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

Christoph Haase
Post-doctoral researcher, VERICONISS project
Piotr Hofman
Post-doctoral researcher, VERICONISS project
Georg Zetzsche
Post-doctoral researcher, DAAD

Ph.D. Students

Michael Blondin
PhD student, Digiteo (joint with U. Montreal, Canada)
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

G. ZetzscheThe complexity of downward closure comparisonsIn ICALP'16, Leibniz International Proceedings in Informatics. Leibniz-Zentrum für Informatik, July 2016. To appear. PDF | BibTeX )
J. Goubault-Larrecq and S. SchmitzDeciding Piecewise Testable Separability for Regular Tree LanguagesIn ICALP'16, Leibniz International Proceedings in Informatics. Leibniz-Zentrum für Informatik, July 2016. To appear. Web page | BibTeX )
S. Göller, C. Haase, R. Lazić and P. TotzkeA Polynomial-Time Algorithm for Reachability in Branching VASS in Dimension OneIn ICALP'16, Leibniz International Proceedings in Informatics. Leibniz-Zentrum für Informatik, July 2016. To appear. Web page | BibTeX )
D. Chistikov and C. HaaseThe Taming of the Semi-Linear SetIn ICALP'16, Leibniz International Proceedings in Informatics. Leibniz-Zentrum für Informatik, July 2016. To appear. PDF | BibTeX )
S. Demri, D. Figueira and M. PraveenReasoning about Data Repetitions with Counter SystemsLogical Methods in Computer Science, 2016. To appear. Web page | PDF | BibTeX )

All the Infini publications