Publications

2025

Conference Articles

1. Formally Verified Hardening of C Programs against Hardware Fault Injection. Basile Pesin, Sylvain Boulmé, David Monniaux, Marie-Laure Potet - 14th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP'25) - [bibtex]

2024

Journal Articles

2. Construire des logiciels fiables. Sylvain Boulmé - Interstices - [bibtex]
3. Self-stabilizing synchronous unison in directed networks. Karine Altisen, Alain Cournier, Geoffrey Defalque, Stéphane Devismes - Theoretical Computer Science - [bibtex]

Conference Articles

4. Chamois: agile development of CompCert extensions for optimization and security. David Monniaux, Sylvain Boulmé - JFLA 2024 -- 35es Journées Francophones des Langages Applicatifs - [bibtex]
5. On Self-stabilizing Leader Election in Directed Networks. Karine Altisen, Alain Cournier, Geoffrey Defalque, Stéphane Devismes - Proceedings of the 43rd ACM Symposium on Principles of Distributed Computing (PODC 2024) - [bibtex]

2023

Journal Articles

6. Formally Verifying Optimizations with Block Simulations. Léo Gourdin, Benjamin Bonneau, Sylvain Boulmé, David Monniaux, Alexandre Bérard - Proceedings of the ACM on Programming Languages, Issue OOPSLA2 - [bibtex]

Conference Articles

7. Complexité certifiée d'algorithmes autostabilisants en rondes. Karine Altisen, Pierre Corbineau, Stéphane Devismes - ALGOTEL 2023 - 25èmes Rencontres Francophones sur les Aspects Algorithmiques des Télécommunications - [bibtex]
8. Lazy Code Transformations in a Formally Verified Compiler. Léo Gourdin - ICOOOLPS '23: 18th ACM International Workshop on Implementation, Compilation, Optimization of OO Languages, Programs and Systems - [bibtex]
9. Testing a Formally Verified Compiler. David Monniaux, Léo Gourdin, Sylvain Boulmé, Olivier Lebeltel - Tests and Proofs (TAP 2023) - [bibtex]
10. Self-stabilizing Synchronous Unison in Directed Networks. Karine Altisen, Alain Cournier, Geoffrey Defalque, Stéphane Devismes - Proceedings of the 24th International Conference on Distributed Computing and Networking (ICDCN 2023) - Best Student Paper Award - [bibtex]

2022

Conference Articles

11. The Trusted Computing Base of the CompCert Verified Compiler. David Monniaux, Sylvain Boulmé - Programming Languages and Systems (ESOP 2022) - [bibtex]
12. Formally Verified Superblock Scheduling. Cyril Six, Léo Gourdin, Sylvain Boulmé, David Monniaux, Justus Fasse, Nicolas Nardino - Certified Programs and Proofs (CPP '22) - [bibtex]
13. A CompCert Backend with Symbolic Encryption. Paolo Torrini, Sylvain Boulmé - Sixth workshop on Principles of Secure Compilation (PriSC'22), part of the 49th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2022) - [bibtex]

2021

Conference Articles

14. Exact Worst Case Self-Stabilization Time. Karine Altisen, Pierre Corbineau, Stéphane Devismes - ICDCN '21: International Conference on Distributed Computing and Networking, Virtual Event, Nara, Japan, January 5-8, 2021 - [bibtex]
15. Simple, light, yet formally verified, global common subexpression elimination and loop-invariant code motion. David Monniaux, Cyril Six - LCTES '21: 22nd ACM SIGPLAN/SIGBED International Conference on Languages, Compilers, and Tools for Embedded Systems, Virtual Event, Canada, 22 June, 2021 - [bibtex]

PhD Thesis and HDR

16. Formally Verified Defensive Programming (efficient Coq-verified computations from untrusted ML oracles). Sylvain Boulmé - Habilitation Thesis - [bibtex]
17. Optimized and formally-verified compilation for a VLIW processor. Cyril Six - [bibtex]

2020

Journal Articles

18. Virtual timeline: a formal abstraction for verifying preemptive schedulers with temporal isolation. Mengqi Liu, Lionel Rieg, Zhong Shao, Ronghui Gu, David Costanzo, Jung-Eun Kim, Man-Ki Yoon - Proc. ACM Program. Lang. -- POPL 2020 Proceedings - [bibtex]
19. Certified and Efficient Instruction Scheduling: Application to Interlocked VLIW Processors. Cyril Six, Sylvain Boulmé, David Monniaux - Proc. ACM Program. Lang. - [bibtex]

Conference Articles

20. Du discrètement continu au continûment discret. Thibaut Balabonski, Pierre Courtieu, Robin Pelle, Lionel Rieg, Sébastien Tixeuil, Xavier Urbain - ALGOTEL 2020 - 22èmes Rencontres Francophones sur les Aspects Algorithmiques des Télécommunications - [bibtex]

2019

Journal Articles

21. Refinement to Certify Abstract Interpretations: Illustrated on Linearization for Polyhedra. Sylvain Boulmé, Alexandre Maréchal - Journal of Automated Reasoning - [bibtex]

Conference Articles

22. Manuel de savoir-prouver à l'usage des roboteux et des distributeux. Thibaut Balabonski, Pierre Courtieu, Lionel Rieg, Sébastien Tixeuil, Xavier Urbain - ALGOTEL 2019, June 4-7, Proceedings - [bibtex]
23. Integrating Formal Schedulability Analysis into a Verified OS Kernel. Xiaojie Guo, Maxime Lesourd, Mengqi Liu, Lionel Rieg, Zhong Shao - Computer Aided Verification - 31st International Conference, CAV 2019, July 15-18, Proceedings - [bibtex]
24. Continuous vs. Discrete Asynchronous Moves: a Certified Approach for Mobile Robots on Graphs. Thibaut Balabonski, Pierre Courtieu, Robin Pelle, Lionel Rieg, Sébastien Tixeuil, Xavier Urbain - NETYS 2019, June 19-21, Proceedings - [bibtex]

2018

Conference Articles

25. The Verified Polyhedron Library: an overview. Sylvain Boulmé, Alexandre Maréchal, David Monniaux, Michaël P'erin, Hang Yu - 20th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC) - [bibtex]
26. A Coq Tactic for Equality Learning in Linear Arithmetic. Sylvain Boulmé, Alexandre Maréchal - Interactive Theorem Proving - 9th International Conference, ITP 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 9-12, 2018, Proceedings - [bibtex]

2015

Conference Articles

27. Refinement to Certify Abstract Interpretations, Illustrated on Linearization for Polyhedra. Sylvain Boulmé, Alexandre Maréchal - Interactive Theorem Proving - 6th International Conference, ITP 2015, Nanjing, China, August 24-27, 2015, Proceedings - [bibtex]

2014

Conference Articles

28. Modular and lightweight certification of polyhedral abstract domains. Alexis Fouilhé, Sylvain Boulmé, Michaël P'erin - Types for Proofs and Programs (TYPES 2014) -- Book of Abstracts - [bibtex]
29. A Certifying Frontend for (Sub)polyhedral Abstract Domains. Alexis Fouilhé, Sylvain Boulmé - Verified Software: Theories, Tools and Experiments (VSTTE 2014) - [bibtex]