Sylvain Boulmé

22 papers A 1B 5C 1Misc 1Journal 5Unranked 8
YearRankTypeTitle / Venue / Authors
2025 B conf
Formally Verified Hardening of C Programs against Hardware Fault Injection.
CPP
Basile Pesin, Sylvain Boulmé, David Monniaux, Marie-Laure Potet
2023 J jnl
Formally Verifying Optimizations with Block Simulations.
Proc. ACM Program. Lang.
Léo Gourdin, Benjamin Bonneau, Sylvain Boulmé, David Monniaux, Alexandre Bérard
2023 C conf
Testing a Formally Verified Compiler.
TAP
David Monniaux, Léo Gourdin, Sylvain Boulmé, Olivier Lebeltel
2022 B conf
Formally verified superblock scheduling.
CPP
Cyril Six, Léo Gourdin, Sylvain Boulmé, David Monniaux, Justus Fasse, Nicolas Nardino
2022 A conf
The Trusted Computing Base of the CompCert Verified Compiler.
ESOP
David Monniaux, Sylvain Boulmé
2022 J jnl
The Trusted Computing Base of the CompCert Verified Compiler.
CoRR
David Monniaux, Sylvain Boulmé
2021 — book
Formally Verified Defensive Programming (efficient Coq-verified computations from untrusted ML oracles). (Programmation défensive formellement vérifiée (calculs efficaces et vérifiés en Coq, à partir d'oracles OCaml potentiellement non fiables)).
Sylvain Boulmé
2020 J jnl
Certified and efficient instruction scheduling: application to interlocked VLIW processors.
Proc. ACM Program. Lang.
Cyril Six, Sylvain Boulmé, David Monniaux
2019 J jnl
Refinement to Certify Abstract Interpretations: Illustrated on Linearization for Polyhedra.
J. Autom. Reason.
Sylvain Boulmé, Alexandre Maréchal
2018 B conf
A Coq Tactic for Equality Learning in Linear Arithmetic.
ITP
Sylvain Boulmé, Alexandre Maréchal
2018 Misc conf
The Verified Polyhedron Library: an Overview.
SYNASC
Sylvain Boulmé, Alexandre Maréchal, David Monniaux, Michaël Périn, Hang Yu
2015 B conf
Refinement to Certify Abstract Interpretations, Illustrated on Linearization for Polyhedra.
ITP
Sylvain Boulmé, Alexandre Maréchal
2014 — conf
A Certifying Frontend for (Sub)polyhedral Abstract Domains.
VSTTE
Alexis Fouilhé, Sylvain Boulmé
2010 — conf
A Refinement Methodology for Object-Oriented Programs.
FoVeOOS
Asma Tafat, Sylvain Boulmé, Claude Marché
2009 — conf
Relaxing Restrictions on Invariant Composition in the B Method by Ownership Control
Rigorous Methods for Software Construction and Analysis
Sylvain Boulmé, Marie-Laure Potet
2007 — conf
Interpreting Invariant Composition in the B Method Using the Spec# Ownership Relation: A Way to Explain and Relax B Restrictions.
B
Sylvain Boulmé, Marie-Laure Potet
2007 — conf
Intuitionistic Refinement Calculus.
TLCA
Sylvain Boulmé
2005 — conf
Proof Contexts with Late Binding.
TLCA
Virgile Prevosto, Sylvain Boulmé
2004 J jnl
Adaptabilité et validation de la traduction de B vers C. Points de vue et résultats du projet BOM.
Tech. Sci. Informatiques
Frédéric Badeau, Didier Bert, Sylvain Boulmé, Christophe Métayer, Marie-Laure Potet, Nicolas Stouls, Laurent Voisin
2003 — conf
Adaptable Translator of B Specifications to Embedded C Programs.
FME
Didier Bert, Sylvain Boulmé, Marie-Laure Potet, Antoine Requet, Laurent Voisin
2001 B conf
Certifying Synchrony for Free.
LPAR
Sylvain Boulmé, Grégoire Hamon
1999 — conf
On the way to certify Computer Algebra Systems.
Calculemus
Sylvain Boulmé, Thérèse Hardin, Daniel Hirschkoff, Valérie Ménissier-Morain, Renaud Rioboo