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 and PhD proposals are regularly posted by LSV researchers on our themes.
the scientific report for the 5-year contract 2014--2018 [in French]
|•||. Unboxing Mutually Recursive Type Definitions. In JFLA'19. January 2019. To appear. ( PDF | BibTeX )|
|•||. Abstract Representation of Binders in OCaml using the Bindlib Library. In LFMTP'18, pages 42-56. ACM Press, July 2018. ( Web page | PDF | BibTeX )|
|•||. PML2: Integrated Program Verification in ML. In TYPES'17, Leibniz International Proceedings in Informatics. Leibniz-Zentrum für Informatik, 2018. To appear. ( PDF | BibTeX )|
|•||. Practical Subtyping for Curry-Style Languages. ACM Transactions on Programming Languages and Systems, 2018. To appear. ( PDF | BibTeX )|
|•||. Reasoning about reversal-bounded counter machines. In Ewa Orlowska on Relational Methods in Logic and Computer Science, Outstanding Contributions to Logic 17, pages 441-479. Springer, December 2018. ( PDF | BibTeX )|