| [j2] | Martin Clochard, Léon Gondelman, and Mário Pereira. The Matrix Reproved (Verification Pearl). Journal of Automated Reasoning, October, 2017. [ DOI | .pdf ] |
| [j1] | Jean-Christophe Filliâtre, Léon Gondelman, and Andrei Paskevich. The spirit of ghost code. Formal Methods in System Design, 48(3):152--174, 2016. [ bib | DOI | full text on HAL ] |
| [c4] | Dan Frumin, Léon Gondelman, and Robbert Krebbers. Semi-automated reasoning about non-determinism in C expressions. European Symposium on Programming (ESOP), 2019 (TO APPEAR). [ .pdf ] |
| [c3] | Dan Frumin, Léon Gondelman, Herman Geuvers, and Niels van der Weide. Finite Sets in Homotopy Type Theory. Certified Programs and Proofs (CPP), 2018. [ .pdf ] |
| [c2] | Martin Clochard, Léon Gondelman, and Mário Pereira. The Matrix reproved. In Sandrine Blazy and Marsha Chechik, editors, 8th Working Conference on Verified Software: Theories, Tools and Experiments (VSTTE), Lecture Notes in Computer Science, Toronto, Canada, July 2016. Springer. [ bib | full text on HAL ] |
| [c1] | Jean-Christophe Filliâtre, Léon Gondelman, and Andrei Paskevich. The spirit of ghost code. In Armin Biere and Roderick Bloem, editors, 26th International Conference on Computer Aided Verification, volume 8859 of Lecture Notes in Computer Science, pages 1--16, Vienna, Austria, July 2014. Springer. [ bib | full text on HAL | .pdf ] |
| [n1] | Martin Clochard and Léon Gondelman. Double WP: vers une preuve automatique d'un compilateur. In Vingt-sixièmes Journées Francophones des Langages Applicatifs, Val d'Ajol, France, January 2015. [ bib | full text on HAL ] |
| [s1] | Jean-Christophe Filliâtre, Léon Gondelman, Andrei Paskevich, and Mário Pereira. A Toolchain for Verified OCaml Programs. Current status (Fall 2017): submitted. [ .pdf ] |
| [r2] | Léon Gondelman. Un système de types pragmatique pour la vérification déductive des programmes. PhD Thesis, Université Paris Sud, December 2016. [ .pdf ] |
| [r1] | Jean-Christophe Filliâtre, Léon Gondelman, and Andrei Paskevich. A pragmatic type system for deductive verification. Research report, Université Paris Sud, 2016. [ bib | full text on HAL ] |