Recherche - Archive ouverte HAL Accéder directement au contenu

Filtrer vos résultats

17 résultats
Page :
triés par
Image document

Formally Verifying Optimizations with Block Simulations

 Léo Gourdin , Benjamin Bonneau , Sylvain Boulmé , David Monniaux , Alexandre Bérard
Proceedings of the ACM on Programming Languages, 2023, 7 (OOPSLA2), pp.59-88. ⟨10.1145/3622799⟩
Article dans une revue hal-04102940v3
Image document

Certified and efficient instruction scheduling. Application to interlocked VLIW processors.

 Cyril Six , Sylvain Boulmé , David Monniaux
Proceedings of the ACM on Programming Languages, 2020, OOPSLA 2020, pp.129. ⟨10.1145/3428197⟩
Article dans une revue hal-02185883v3
Image document

Formally Verified Superblock Scheduling

 Cyril Six , Léo Gourdin , Sylvain Boulmé , David Monniaux , Justus Fasse , et al.
Certified Programs and Proofs (CPP ’22), Jan 2022, Philadelphia, United States. pp.40-54, ⟨10.1145/3497775.3503679⟩
Communication dans un congrès hal-03200774v2
Image document

A Coq Tactic for Equality Learning in Linear Arithmetic

 Sylvain Boulmé , Alexandre Maréchal
Interactive Theorem Proving - 9th International Conference, (ITP 2018), Jul 2018, Oxford, United Kingdom. ⟨10.1007/978-3-319-94821-8_7⟩
Communication dans un congrès hal-01505598v2
Image document

The Trusted Computing Base of the CompCert Verified Compiler

 David Monniaux , Sylvain Boulmé
Programming Languages and Systems (ESOP 2022), Apr 2022, Munich, Germany. pp.204-233, ⟨10.1007/978-3-030-99336-8_8⟩
Communication dans un congrès hal-03541595v2
Image document

Testing a Formally Verified Compiler

 David Monniaux , Léo Gourdin , Sylvain Boulmé , Olivier Lebeltel
Tests and Proofs (TAP 2023), Jul 2023, Leicester, United Kingdom. pp.40-48, ⟨10.1007/978-3-031-38828-6_3⟩
Communication dans un congrès hal-04096390v1
Image document

Construire des logiciels fiables

 Sylvain Boulmé
Interstices, 2024
Article dans une revue hal-04438448v1
Image document

Toward Certification for Free!

 Sylvain Boulmé , Alexandre Maréchal
2017
Pré-publication, Document de travail hal-01558252v3
Image document

A refinement methodology for object-oriented programs

 Asma Tafat , Sylvain Boulmé , Claude Marché
Formal Verification of Object-Oriented Software, Jun 2010, Paris, France. pp.143--159
Communication dans un congrès inria-00534336v1
Image document

A CompCert Backend with Symbolic Encryption

 Paolo Torrini , Sylvain Boulmé
Sixth workshop on Principles of Secure Compilation (PriSC'22), part of the 49th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2022), Jan 2022, Philadelphia, Pennsylvania, United States
Communication dans un congrès hal-03555551v1
Image document

Chamois: agile development of CompCert extensions for optimization and security

 David Monniaux , Sylvain Boulmé
35es Journées Francophones des Langages Applicatifs (JFLA 2024), Jan 2024, Saint-Jacut-de-la-Mer, France
Communication dans un congrès hal-04406465v1
Image document

A Refinement Approach for Correct-by-Construction Object-Oriented Programs

 Asma Tafat , Sylvain Boulmé , Claude Marché
[Research Report] RR-7310, INRIA. 2010, pp.31
Rapport inria-00491835v1
Image document

Formally Verified Defensive Programming (efficient Coq-verified computations from untrusted ML oracles)

 Sylvain Boulmé
Software Engineering [cs.SE]. Université Grenoble-Alpes, 2021
HDR tel-03356701v1
Image document

Refinement to Certify Abstract Interpretations, Illustrated on Linearization for Polyhedra

 Sylvain Boulmé , Alexandre Maréchal
Journal of Automated Reasoning, 2018, ⟨10.1007/s10817-018-9492-2⟩
Article dans une revue hal-01133865v4
Image document

Embedding Untrusted Imperative ML Oracles into Coq Verified Code

 Sylvain Boulmé , Thomas Vandendorpe
2019
Pré-publication, Document de travail hal-02062288v2

Adaptabilité et validation de la traduction de B vers C - Points de vue du projet BOM

 Frédéric Badeau , Didier Bert , Sylvain Boulmé , Claude Métayer , Marie-Laure Potet , et al.
Revue des Sciences et Technologies de l'Information - Série TSI : Technique et Science Informatiques, 2004, Approches Formelles pour le Développement de Logiciels, 23 (7), pp.879--903. ⟨10.3166/tsi.23.879-903⟩
Article dans une revue istex inria-00384177v1

Traduction de B vers des langages de programmation

 Frédéric Badeau , Didier Bert , Sylvain Boulmé , Claude Métayer , Marie-Laure Potet , et al.
Approches Formelles dans l'Assistance au Développement de Logiciels (AFADL'03), IRISA, Jan 2003, Rennes, France. pp.87--102
Communication dans un congrès inria-00392235v1
Page :