Adaptable translator of B specifications to embedded C programs D Bert, S Boulmé, ML Potet, A Requet, L Voisin International Symposium of Formal Methods Europe, 94-113, 2003 | 64 | 2003 |
Certifying synchrony for free S Boulmé, G Hamon International Conference on Logic for Programming Artificial Intelligence …, 2001 | 49 | 2001 |
Certified and efficient instruction scheduling: application to interlocked VLIW processors C Six, S Boulmé, D Monniaux Proceedings of the ACM on Programming Languages 4 (OOPSLA), 1-29, 2020 | 30 | 2020 |
A certifying frontend for (sub) polyhedral abstract domains A Fouilhé, S Boulmé Verified Software: Theories, Tools and Experiments: 6th International …, 2014 | 30 | 2014 |
Spécification d'un environnement dédié à la programmation certifiée de bibliothèques de Calcul Formel S Boulmé Paris 6, 2000 | 24 | 2000 |
On the way to certify computer algebra systems S Boulmé, T Hardin, D Hirschkoff, V Ménissier-Morain, R Rioboo Electronic Notes in Theoretical Computer Science 23 (3), 370-385, 1999 | 22 | 1999 |
Some hints for polynomials in the Foc project S Boulmé, T Hardin, R Rioboo Calculemus 2001, 142-154, 2001 | 21 | 2001 |
The verified polyhedron library: an overview S Boulmé, A Marechaly, D Monniaux, M Périn, H Yu 2018 20th International Symposium on Symbolic and Numeric Algorithms for …, 2018 | 19 | 2018 |
Intuitionistic refinement calculus S Boulmé Typed Lambda Calculi and Applications: 8th International Conference, TLCA …, 2007 | 19 | 2007 |
Formally verifying optimizations with block simulations L Gourdin, B Bonneau, S Boulmé, D Monniaux, A Bérard Proceedings of the ACM on Programming Languages 7 (OOPSLA2), 59-88, 2023 | 17 | 2023 |
Formally verified superblock scheduling C Six, L Gourdin, S Boulmé, D Monniaux, J Fasse, N Nardino Proceedings of the 11th ACM SIGPLAN International Conference on Certified …, 2022 | 15 | 2022 |
Interpreting invariant composition in the B method using the Spec# ownership relation: a way to explain and relax B restrictions S Boulmé, ML Potet International Conference of B Users, 4-18, 2007 | 15 | 2007 |
The trusted computing base of the CompCert verified compiler D Monniaux, S Boulmé European Symposium on Programming, 204-233, 2022 | 13 | 2022 |
A refinement methodology for object-oriented programs A Tafat, S Boulmé, C Marché Formal Verification of Object-Oriented Software: International Conference …, 2011 | 12 | 2011 |
Testing a formally verified compiler D Monniaux, L Gourdin, S Boulmé, O Lebeltel International Conference on Tests and Proofs, 40-48, 2023 | 11 | 2023 |
Formally Verified Defensive Programming (efficient Coq-verified computations from untrusted ML oracles) S Boulmé Université Grenoble-Alpes, 2021 | 11 | 2021 |
Polymorphic Data Types, Objects, Modules and Functors: is it too. much.? S Boulmé, T Hardin, R Rioboo LIP6, 2000 | 10 | 2000 |
Refinement to certify abstract interpretations, illustrated on linearization for polyhedra S Boulmé, A Maréchal Interactive Theorem Proving: 6th International Conference, ITP 2015, Nanjing …, 2015 | 9 | 2015 |
Proof contexts with late binding V Prevosto, S Boulmé Typed Lambda Calculi and Applications: 7th International Conference, TLCA …, 2005 | 7 | 2005 |
A clocked denotational semantics for Lucid-Synchrone in Coq S Boulmé, G Hamon Rap. tech., LIP6, 2001 | 7 | 2001 |