Publications
2025
Articles de conférence
-
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
Articles de revue
-
Construire des logiciels fiables.
Sylvain Boulmé
- Interstices
- [bibtex]
-
Self-stabilizing synchronous unison in directed networks.
Karine Altisen, Alain Cournier, Geoffrey Defalque, Stéphane Devismes
- Theoretical Computer Science
- [bibtex]
Articles de conférence
-
Chamois: agile development of CompCert extensions for optimization and security.
David Monniaux, Sylvain Boulmé
- JFLA 2024 -- 35es Journées Francophones des Langages Applicatifs
- [bibtex]
-
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
Articles de revue
-
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]
Articles de conférence
-
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]
-
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]
-
Testing a Formally Verified Compiler.
David Monniaux, Léo Gourdin, Sylvain Boulmé, Olivier Lebeltel
- Tests and Proofs (TAP 2023)
- [bibtex]
-
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
Articles de conférence
-
The Trusted Computing Base of the CompCert Verified Compiler.
David Monniaux, Sylvain Boulmé
- Programming Languages and Systems (ESOP 2022)
- [bibtex]
-
Formally Verified Superblock Scheduling.
Cyril Six, Léo Gourdin, Sylvain Boulmé, David Monniaux, Justus Fasse, Nicolas Nardino
- Certified Programs and Proofs (CPP '22)
- [bibtex]
-
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
Articles de conférence
-
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]
-
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]
Thèse de doctorat et HDR
-
Formally Verified Defensive Programming (efficient Coq-verified computations from untrusted ML oracles).
Sylvain Boulmé
- Habilitation Thesis
- [bibtex]
-
Optimized and formally-verified compilation for a VLIW processor.
Cyril Six
- [bibtex]
2020
Articles de revue
-
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]
-
Certified and Efficient Instruction Scheduling: Application to Interlocked VLIW Processors.
Cyril Six, Sylvain Boulmé, David Monniaux
- Proc. ACM Program. Lang.
- [bibtex]
Articles de conférence
-
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
Articles de revue
-
Refinement to Certify Abstract Interpretations: Illustrated on Linearization for Polyhedra.
Sylvain Boulmé, Alexandre Maréchal
- Journal of Automated Reasoning
- [bibtex]
Articles de conférence
-
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]
-
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]
-
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
Articles de conférence
-
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]
-
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
Articles de conférence
-
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
Articles de conférence
-
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]
-
A Certifying Frontend for (Sub)polyhedral Abstract Domains.
Alexis Fouilhé, Sylvain Boulmé
- Verified Software: Theories, Tools and Experiments (VSTTE 2014)
- [bibtex]
Navigation