Sylvain Boulmé

Publication Activity (10 Years)

Years Active: 1999-2023
Publications (10 Years): 9

Top Topics

Convex Polyhedra

Detailed Discussion

Remote Attestation

Top Venues

Proc. ACM Program. Lang.

Publications

David Monniaux, Léo Gourdin, Sylvain Boulmé, Olivier Lebeltel
Testing a Formally Verified Compiler. TAP (2023)
Léo Gourdin, Benjamin Bonneau, Sylvain Boulmé, David Monniaux, Alexandre Bérard
Formally Verifying Optimizations with Block Simulations. Proc. ACM Program. Lang. 7 (OOPSLA2) (2023)
David Monniaux, Sylvain Boulmé
The Trusted Computing Base of the CompCert Verified Compiler. CoRR (2022)
David Monniaux, Sylvain Boulmé
The Trusted Computing Base of the CompCert Verified Compiler. ESOP (2022)
Cyril Six, Léo Gourdin, Sylvain Boulmé, David Monniaux, Justus Fasse, Nicolas Nardino
Formally verified superblock scheduling. CPP (2022)
Cyril Six, Sylvain Boulmé, David Monniaux
Certified and efficient instruction scheduling: application to interlocked VLIW processors. Proc. ACM Program. Lang. 4 (OOPSLA) (2020)
Sylvain Boulmé, Alexandre Maréchal
Refinement to Certify Abstract Interpretations: Illustrated on Linearization for Polyhedra. J. Autom. Reason. 62 (4) (2019)
Sylvain Boulmé, Alexandre Maréchal
A Coq Tactic for Equality Learning in Linear Arithmetic. ITP (2018)
Sylvain Boulmé, Alexandre Maréchal, David Monniaux, Michaël Périn, Hang Yu
The Verified Polyhedron Library: an Overview. SYNASC (2018)
Sylvain Boulmé, Alexandre Maréchal
Refinement to Certify Abstract Interpretations, Illustrated on Linearization for Polyhedra. ITP (2015)
Alexis Fouilhé, Sylvain Boulmé
A Certifying Frontend for (Sub)polyhedral Abstract Domains. VSTTE (2014)
Asma Tafat, Sylvain Boulmé, Claude Marché
A Refinement Methodology for Object-Oriented Programs. FoVeOOS (2010)
Sylvain Boulmé, Marie-Laure Potet
Spec#. Rigorous Methods for Software Construction and Analysis (2009)
Sylvain Boulmé
Intuitionistic Refinement Calculus. TLCA (2007)
Sylvain Boulmé, Marie-Laure Potet
Interpreting Invariant Composition in the B Method Using the Spec# Ownership Relation: A Way to Explain and Relax B Restrictions. B (2007)
Virgile Prevosto, Sylvain Boulmé
Proof Contexts with Late Binding. TLCA (2005)
Frédéric Badeau, Didier Bert, Sylvain Boulmé, Christophe Métayer, Marie-Laure Potet, Nicolas Stouls, Laurent Voisin
Adaptabilité et validation de la traduction de B vers C. Points de vue et résultats du projet BOM. Tech. Sci. Informatiques 23 (7) (2004)
Didier Bert, Sylvain Boulmé, Marie-Laure Potet, Antoine Requet, Laurent Voisin
Adaptable Translator of B Specifications to Embedded C Programs. FME (2003)
Sylvain Boulmé, Grégoire Hamon
Certifying Synchrony for Free. LPAR (2001)
Sylvain Boulmé, Thérèse Hardin, Daniel Hirschkoff, Valérie Ménissier-Morain, Renaud Rioboo
On the way to certify Computer Algebra Systems. Calculemus (1999)