 |
 |
 |
|
|
||
|---|---|---|
| hal-01512286v1
Conference papers
A Formally Verified Compiler for Lustre PLDI 2017 - 38th ACM SIGPLAN Conference on Programming Language Design and Implementation, ACM, Jun 2017, Barcelone, Spain |
||
| hal-01091802v8
Reports
The CompCert C verified compiler: Documentation and user’s manual [Intern report] Inria. 2020, pp.1-78 |
||
| hal-02392159v2
Books
Software, between mind and matter Collège de France, 2020, Inaugural lecture at Collège de France |
||
| hal-00930213v7
Reports
The OCaml system release 4.11: Documentation and user's manual [Intern report] Inria. 2020, pp.1-820 |
||
| hal-02405754v1
Books
Le logiciel, entre l’esprit et la matière OpenEdition Books, 2019, 9782722605299 |
||
| hal-02370113v1
Books
Le logiciel, entre l'esprit et la matière Fayard, 284, 2019, Leçons inaugurales du Collège de France, 978-2-213-71241-3 |
||
| hal-02392114v1
Conference papers
In Search of Software Perfection BOB Summer 2019 Konferenz, Aug 2019, Berlin, Germany |
||
| inria-00289549v1
Conference papers
A structured approach to proving compiler optimizations based on dataflow analysis Types for Proofs and Programs, Workshop TYPES 2004, Dec 2004, Jouy-en-Josas, France. pp.66-81, ⟨10.1007/11617990⟩ |
||
| inria-00289709v1
Journal articles
Tilting at windmills with Coq: formal verification of a compilation algorithm for parallel moves Journal of Automated Reasoning, Springer Verlag, 2008, 40 (4), pp.307-326. ⟨10.1007/s10817-007-9096-8⟩ |
||
| inria-00176007v1
Preprints, Working Papers, ...
Battling windmills with Coq: formal verification of a compilation algorithm for parallel moves 2007 |
||
| hal-01848686v1
Conference papers
Embedded Program Annotations for WCET Analysis WCET 2018: 18th International Workshop on Worst-Case Execution Time Analysis, Jul 2018, Barcelona, Spain. ⟨10.4230/OASIcs.WCET.2018.8⟩ |
||
| hal-01620870v1
Other publications
How I found a crash bug with hyperthreading in Intel's Skylake processors 2017 |
||
|
|
||
| hal-01238879v1
Conference papers
CompCert - A Formally Verified Optimizing Compiler ERTS 2016: Embedded Real Time Software and Systems, 8th European Congress, SEE, Jan 2016, Toulouse, France |
||
| hal-00905435v1
Book sections
The CompCert memory model Appel, Andrew W. Program Logics for Certified Compilers, Cambridge University Press, pp.237-271, 2014, 9781107048010 |
||
| hal-01078386v1
Conference papers
A formally-verified C static analyzer POPL 2015: 42nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Jan 2015, Mumbai, India. pp.247-259, ⟨10.1145/2676726.2676966⟩ |
||
| hal-01643290v1
Conference papers
CompCert: Practical Experience on Integrating and Qualifying a Formally Verified Optimizing Compiler ERTS2 2018 - 9th European Congress Embedded Real-Time Software and Systems, 3AF, SEE, SIE, Jan 2018, Toulouse, France. pp.1-9 |
||
| inria-00077921v1
Conference papers
Formal verification of a memory model for C-like imperative languages ICFEM'05: 7th International Conference on Formal Engineering Methods, Nov 2005, Manchester, United Kingdom. pp.280-299, ⟨10.1007/11576280⟩ |
||
| hal-00862689v3
Journal articles
Verified Compilation of Floating-Point Computations Journal of Automated Reasoning, Springer Verlag, 2015, 54 (2), pp.135-163. ⟨10.1007/s10817-014-9317-x⟩ |
||
| inria-00415865v1
Conference papers
Verified Validation of Lazy Code Motion ACM SIGPLAN conference on Programming Language Design and Implementation (PLDI), Jun 2009, Dublin, Ireland. pp.316-326, ⟨10.1145/1542476.1542512⟩ |
||
| hal-01059423v1
Conference papers
Formal proofs of code generation and verification tools SEFM 2014 - 12th International Conference Software Engineering and Formal Methods, Sep 2014, Grenoble, France. pp.1-4, ⟨10.1007/978-3-319-10431-7_1⟩ |
||
| hal-00773109v1
Conference papers
A formally-verified alias analysis CPP 2012 - Second International Conference on Certified Programs and Proofs, Dec 2012, Kyoto, Japan. pp.11-26, ⟨10.1007/978-3-642-35308-6_5⟩ |
||
| hal-00703441v1
Reports
The CompCert Memory Model, Version 2 [Research Report] RR-7987, INRIA. 2012, pp.26 |
||
| hal-01077321v1
Conference papers
Validating LR(1) Parsers ESOP 2012 - Programming Languages and Systems - 21st European Symposium on Programming, Mar 2012, Tallinn, Estonia. pp.397-416, ⟨10.1007/978-3-642-28869-2_20⟩ |
||
| inria-00289540v1
Conference papers
Formal verification of translation validators: A case study on instruction scheduling optimizations 35th ACM Symposium on Principles of Programming Languages (POPL 2008), ACM, Jan 2008, San Francisco, United States. pp.17-27, ⟨10.1145/1328438.1328444⟩ |
||
| inria-00309010v1
Journal articles
Coinductive big-step operational semantics Information and Computation, Elsevier, 2009, 207 (2), pp.284-304. ⟨10.1016/j.ic.2007.12.004⟩ |
||
| inria-00106401v1
Conference papers
Formal Verification of a C Compiler Front-end FM'06: 14th Symposium on Formal Methods, Aug 2006, Hamilton, Canada. pp.460-475, ⟨10.1007/11813040_31⟩ |
||
| hal-00981212v1
Conference papers
Formal C semantics: CompCert and the C standard ITP 2014: Fifth conference on Interactive Theorem Proving, Jul 2014, Vienna, Austria. pp.543-548, ⟨10.1007/978-3-319-08970-6_36⟩ |
||
| hal-00674174v1
Conference papers
Formal verification of object layout for C++ multiple inheritance POPL'11 - 38th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, ACM, Jan 2011, Austin, TX, United States. pp.67-79, ⟨10.1145/1926385.1926395⟩ |
||
| hal-00653367v1
Conference papers
Formally verified optimizing compilation in ACG-based flight control software ERTS2 2012: Embedded Real Time Software and Systems, AAAF, SEE, Feb 2012, Toulouse, France |
||
|
|
||