Research at LSV

Research at LSV focuses on the verification of computerized systems, of databases and of security protocols. LSV develops the mathematical and algorithmic foundations to the development of tools for automatically proving correctness and detecting flaws.

Internship Proposals at LSV

Go to the internships page

Internship and PhD proposals are regularly posted by LSV researchers on our themes.

Research axes

About LSV


Internship opportunities

the scientific report for the 5-year contract 2014--2018 [in French]

the LSV book: LSV bookSystems and Software Verification. Model-Checking Techniques and Tools

Recent Publications

All the LSV publications

S. Colin, R. Lepigre and G. SchererUnboxing Mutually Recursive Type DefinitionsIn JFLA'19. January 2019. To appear. PDF | BibTeX )
R. Lepigre and C. RaffalliAbstract Representation of Binders in OCaml using the Bindlib LibraryIn LFMTP'18, pages 42-56. ACM Press, July 2018. Web page | PDF | BibTeX )
R. LepigrePML2: Integrated Program Verification in MLIn TYPES'17, Leibniz International Proceedings in Informatics. Leibniz-Zentrum für Informatik, 2018. To appear. PDF | BibTeX )
R. Lepigre and C. RaffalliPractical Subtyping for Curry-Style LanguagesACM Transactions on Programming Languages and Systems, 2018. To appear. PDF | BibTeX )
S. DemriReasoning about reversal-bounded counter machinesIn Ewa Orlowska on Relational Methods in Logic and Computer Science, Outstanding Contributions to Logic 17, pages 441-479. Springer, December 2018. PDF | BibTeX )

All the LSV publications