Sylvain Boulmé

Orcid: 0000-0002-9501-9606

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

Collaborative distances:
  • Dijkstra number2 of four.
  • Erdős number3 of four.

Timeline

Legend:

Book 
In proceedings 
Article 
PhD thesis 
Dataset
Other 

Links

On csauthors.net:

Bibliography

2023
Formally Verifying Optimizations with Block Simulations.
Proc. ACM Program. Lang., October, 2023

Testing a Formally Verified Compiler.
Proceedings of the Tests and Proofs - 17th International Conference, 2023

2022
The Trusted Computing Base of the CompCert Verified Compiler.
Proceedings of the Programming Languages and Systems, 2022

Formally verified superblock scheduling.
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)).
, 2021

2020
Certified and efficient instruction scheduling: application to interlocked VLIW processors.
Proc. ACM Program. Lang., 2020

2019
Refinement to Certify Abstract Interpretations: Illustrated on Linearization for Polyhedra.
J. Autom. Reason., 2019

2018
The Verified Polyhedron Library: an Overview.
Proceedings of the 20th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, 2018

A Coq Tactic for Equality Learning in Linear Arithmetic.
Proceedings of the Interactive Theorem Proving - 9th International Conference, 2018

2014
A Certifying Frontend for (Sub)polyhedral Abstract Domains.
Proceedings of the Verified Software: Theories, Tools and Experiments, 2014

2010
A Refinement Methodology for Object-Oriented Programs.
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#.
Proceedings of the Rigorous Methods for Software Construction and Analysis, 2009

2007
Intuitionistic Refinement Calculus.
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.
Proceedings of the B 2007: Formal Specification and Development in B, 2007

2005
Proof Contexts with Late Binding.
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.
Tech. Sci. Informatiques, 2004

2003
Adaptable Translator of B Specifications to Embedded C Programs.
Proceedings of the FME 2003: Formal Methods, 2003

2001
Certifying Synchrony for Free.
Proceedings of the Logic for Programming, 2001

1999
On the way to certify Computer Algebra Systems.
Proceedings of the Systems for Integrated Computation and Deduction, 1999


  Loading...