Sylvain Boulmé

According to our database, Sylvain Boulmé authored at least 19 papers between 1999 and 2023.

Collaborative distances:

• Dijkstra number of four.
• Erdős number of four.

2023

Formally Verifying Optimizations with Block Simulations.

Léo Gourdin, Benjamin Bonneau, Sylvain Boulmé, David Monniaux, Alexandre Bérard

Proc. ACM Program. Lang., October, 2023

Testing a Formally Verified Compiler.

David Monniaux, Léo Gourdin, Sylvain Boulmé, Olivier Lebeltel

Proceedings of the Tests and Proofs - 17th International Conference, 2023

2022

The Trusted Computing Base of the CompCert Verified Compiler.

David Monniaux, Sylvain Boulmé

Proceedings of the Programming Languages and Systems, 2022

Formally verified superblock scheduling.

Cyril Six, Léo Gourdin, Sylvain Boulmé, David Monniaux, Justus Fasse, Nicolas Nardino

Proceedings of the CPP '22: 11th ACM SIGPLAN International Conference on Certified Programs and Proofs, Philadelphia, PA, USA, January 17, 2022

2021

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é

, 2021

2020

Certified and efficient instruction scheduling: application to interlocked VLIW processors.

Cyril Six, Sylvain Boulmé, David Monniaux

Proc. ACM Program. Lang., 2020

2019

Refinement to Certify Abstract Interpretations: Illustrated on Linearization for Polyhedra.

Sylvain Boulmé, Alexandre Maréchal

J. Autom. Reason., 2019

2018

The Verified Polyhedron Library: an Overview.

Sylvain Boulmé, Alexandre Maréchal, David Monniaux, Michaël Périn, Hang Yu

Proceedings of the 20th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, 2018

A Coq Tactic for Equality Learning in Linear Arithmetic.

Sylvain Boulmé, Alexandre Maréchal

Proceedings of the Interactive Theorem Proving - 9th International Conference, 2018

2014

A Certifying Frontend for (Sub)polyhedral Abstract Domains.

Alexis Fouilhé, Sylvain Boulmé

Proceedings of the Verified Software: Theories, Tools and Experiments, 2014

2010

A Refinement Methodology for Object-Oriented Programs.

Asma Tafat, Sylvain Boulmé, Claude Marché

Proceedings of the Formal Verification of Object-Oriented Software, 2010

2009

Relaxing Restrictions on Invariant Composition in the B Method by Ownership Control <i>a la</i>Spec#.

Sylvain Boulmé, Marie-Laure Potet

Proceedings of the Rigorous Methods for Software Construction and Analysis, 2009

2007

Intuitionistic Refinement Calculus.

Sylvain Boulmé

Proceedings of the Typed Lambda Calculi and Applications, 8th International Conference, 2007

Interpreting Invariant Composition in the B Method Using the Spec# Ownership Relation: A Way to Explain and Relax B Restrictions.

Sylvain Boulmé, Marie-Laure Potet

Proceedings of the B 2007: Formal Specification and Development in B, 2007

2005

Proof Contexts with Late Binding.

Virgile Prevosto, Sylvain Boulmé

Proceedings of the Typed Lambda Calculi and Applications, 7th International Conference, 2005

2004

Adaptabilité et validation de la traduction de B vers C. Points de vue et résultats du projet BOM.

Frédéric Badeau, Didier Bert, Sylvain Boulmé, Christophe Métayer, Marie-Laure Potet, Nicolas Stouls, Laurent Voisin

Tech. Sci. Informatiques, 2004

2003

Adaptable Translator of B Specifications to Embedded C Programs.

Didier Bert, Sylvain Boulmé, Marie-Laure Potet, Antoine Requet, Laurent Voisin

Proceedings of the FME 2003: Formal Methods, 2003

2001

Certifying Synchrony for Free.

Sylvain Boulmé, Grégoire Hamon

Proceedings of the Logic for Programming, 2001

1999

On the way to certify Computer Algebra Systems.

Sylvain Boulmé, Thérèse Hardin, Daniel Hirschkoff, Valérie Ménissier-Morain, Renaud Rioboo

Proceedings of the Systems for Integrated Computation and Deduction, 1999