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

Laurent Doyen
Researcher, CNRS
Sylvain Schmitz
Assistant professor, ENS Cachan
 
Alain Finkel
Professor, ENS Cachan
Philippe Schnoebelen
Senior researcher, CNRS

Associated and Temporary Members

Étienne Lozes
Assistant professor, ENS Cachan
Mahsa Shirmohammadi
PhD student, ULB
 

Ph.D. Students

Rémi Bonnet
PhD student, ENS Cachan
Julien Reichert
PhD student, ENS Cachan
 

About LSV

Recent Publications

All the Infini publications

S. Demri, M. Jurdziński, O. Lachish and R. LazicThe covering and boundedness problems for branching vector addition systemsJournal of Computer and System Sciences, 2012. To appear. PDF | BibTeX )
P. Karandikar and Ph. SchnoebelenCutting Through Regular Post Embedding ProblemsIn CSR'12, LNCS. Springer,  2012. To appear. PDF | PDF (long version) | BibTeX )
L. DoyenGames and Automata: From Boolean to Quantitative Verification.  Mémoire d'habilitation, École Normale Supérieure de Cachan, France,  2012. PDF | BibTeX )
C. Gardent, G. Perrier, Y. Parmentier and S. SchmitzLexical Disambiguation in LTAG using Left ContextIn LTC'11.  2011. Web page | BibTeX )
A. Finkel and J. Goubault-LarrecqForward Analysis for WSTS, Part II: Complete WSTSLogical Methods in Computer Science, 2012. To appear. BibTeX )

All the Infini publications