Armaël Guéneau


Program verification on a capability machine in presence of untrusted code,
This is for now an English version of the JFLA paper, but is currently being expanded. [ pdf ]

Published articles

Cap’ ou pas cap’ ? Preuve de programmes pour une machine à capacités en presence de code inconnu, Aïna Linn Georges, Armaël Guéneau, Thomas van Strydonck, Amin Timany, Alix Trieu, Dominique Devriese, Lars Birkedal, JFLA 2021.
This is a tutorial-style presentation of some of the methodology used in the POPL'21 paper.
[ bib | Coq development | pdf ]

Efficient and provable local capability revocation using uninitialized capabilities, Aïna Linn Georges, Armaël Guéneau, Thomas van Strydonck, Amin Timany, Alix Trieu, Sander Huyghebaert, Dominique Devriese, and Lars Birkedal. POPL 2021.
[ bib | Coq development | pdf ]

Formal Proof and Analysis of an Incremental Cycle Detection Algorithm, Armaël Guéneau, Jacques-Henri Jourdan, Arthur Charguéraud, François Pottier, ITP 2019.
[ bib | software | pdf | at publisher's | slides ]

A Fistful of Dollars: Formalizing Asymptotic Complexity Claims via Deductive Program Verification, Armaël Guéneau, Arthur Charguéraud, François Pottier, ESOP 2018.
[ bib | software | pdf | slides ]

Verified Characteristic Formulae for CakeML, Armaël Guéneau, Magnus O. Myreen, Ramana Kumar, Michael Norrish, ESOP 2017.
[ bib | software (as part of CakeML) | pdf | slides ]

Presentations in peer-reviewed workshops

Towards Complete Stack Safety for Capability Machines, Aïna Linn Georges, Armaël Guéneau, Alix Trieu, Lars Birkedal, PriSC 2021.
[ pdf ]

Procrastination, a proof engineering technique, Armaël Guéneau, Talk proposal, Coq Workshop @ FLoC 2018.
[ bib | software | pdf | slides ]

The ins and outs of iteration in Mezzo, Armaël Guéneau, François Pottier, Jonathan Protzenko, Talk proposal, HOPE 2013.
[ bib | pdf | slides ]


Mechanized Verification of the Correctness and Asymptotic Complexity of Programs, 2019, PhD thesis. [ pdf | defense slides ]

Formal Verification of Asymptotic Complexity Bounds for OCaml Programs, 2015, Internship report. [ pdf | slides ]

Hybrid Separation Logic, 2014, Internship report. [ pdf | slides ]

Typage de protocoles objets en Mezzo, 2013, Internship report. [ pdf ]