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
Sylvain Schmitz
Assistant professor, ENS Paris-Saclay
 
Alain Finkel
Professor, ENS Paris-Saclay
Philippe Schnoebelen
Senior researcher, CNRS

Associated Members

Simon Halfon
ATER, ENS Paris-Saclay
 

Ph.D. Students

Anthony Lick
PhD student, ANR Prodaq
Alessio Mansutti
PhD student, ENS Paris-Saclay
 

Latest News

Simon Halfon will defend his PhD thesis on June 29th at 2pm, 2018.

Sylvain Schmitz has been nominated Junior Member of the Institut Universitaire de France. During his five-year membership term, he will pursue a project on the verification of resource-centric systems.

Alain Finkel and Philippe Schnoebelen received (jointly with Parosh Abdulla and Bengt Johnsson) the CAV award 2017 for introducing well-structured transition systems, a large class of infinite-state systems with important algorithmic properties.

Presentation

We study algorithmic aspects of infinite-state systems. A particular focus has been on the class of well-structured transition systems (WSTS), vector addition systems, heap-manipulating systems and lifo-like infinite-state systems. Let us just mention four kinds of projects in these areas

Algorithmic Applications of Downward-closed Sets

A classical principle in WSTS is to reduce the problem at hand to the computation of ascending chain of upward-closed sets. The underlying well-quasi order (wqo) guarantees that the chain eventually stabilises and each set of the chain can be finitely presented as the upward-closure of finitely many elements. We are currently investigating the algorithmics of downward-closed for which descending chains are also finite. In particular we are study the algorithmic manipulation of downward-closed set in wqo's in terms of finite unions of ideals, which can be seen as downward-closed sets that are irreducible. LOYD This line of research has applicaitons in studying generalisations of WSTS, provide solutions to problems in formal languages theory, yield new techniques for complexity upper bounds for WSTS and give new insights on classical algorithms solving reachability in vector addition systems, just to mention a few. .

Vector addition systems and extensions

Vector addition systems (VAS) form a particular class of well-structured transitions systems running over a finite set of counters. A central problem is the reachability problem. Indeed, a plethora of problems in computer science reduce to VAS reachability, as for instance the satisfiability problem for expressive data logics. We currently study extensions of VAS. A particular focus lies in the study of branching VAS which extends VAS by allowing the counters to be split, thus allowing to model the sharing of ressources but more importantly having applications in various fields like computation linguistics and linear logic but also to logics on XML trees.

Decision Procedures for Separation Logics

We are interested in the analysis of pointer-manipulating programs, which can be seen as a particular class of infinite- state systems. Separation logic is known as an assertion language to perform verification, by extending Hoare-Floyd logic in order to verify programs with mutable data structures. We are studying the decidability and complexity of various fragments of separation logic. So far we have studied the role of first-order quantifiers in the undecidability of plain separation logic, i.e. with points-to predicate, all Boolean connectives and magic wand, but without recursive predicates and more advanced constructs. Our agenda is focused on the development of decision procedures for separation logics with inductive definitions (to describe shapes such as lists, trees or user-defined recursive structures) and with quantitative properties about the memory cells such as data values or access permissions. In particular, being able to tame fragments of separation logics with the magic wand is one of our major goals.

LIFO-like Infinite-State Systems

Another important class of infinite-state systems in the focus of our research are LIFO-like infinite state systems, i.e. finite-state machines that can manipulate an unbounded data structure in a last-in first-out fashion -- thus faithfully allowing to model recursion in computer programs. We study elementary questions like the reachability problem on such models, but also investigate the computational complexity of deciding the behavioral equivalence between such systems.

Funding

Current Projects

Past Projects

About LSV

Presentation of Infini

Infini presentation at AERES (2013)

Recent Publications

All the Infini publications

D. Baelde, A. Lick and S. SchmitzDecidable XPath Fragments in the Real WorldIn PODS'19. ACM Press, June 2019. To appear. Web page | BibTeX )
P. Karandikar and Ph. SchnoebelenThe height of piecewise-testable languages and the complexity of the logic of subwordsLogical Methods in Computer Science, 2019. To appear. Web page | PDF | BibTeX )
S. DemriOn temporal and separation logicsIn TIME'18, Leibniz International Proceedings in Informatics, pages 1:1-1:4. Leibniz-Zentrum für Informatik, October 2018. Web page | BibTeX )
M. HilaireComplexity of the reachability problem for parametric timed automata.  Rapport de Master, Master Parisien de Recherche en Informatique, Paris, France, September 2018. BibTeX )
D. Baelde, A. Lick and S. SchmitzA Hypersequent Calculus with Clusters for Tense Logic over OrdinalsIn FSTTCS'18, Leibniz International Proceedings in Informatics. Leibniz-Zentrum für Informatik, December 2018. To appear. Web page | BibTeX )

All the Infini publications