Armaël Guéneau

Preprints

Cerise: Program Verification on a Capability Machine in Presence of Untrusted Code. Aïna Linn Georges, Armaël Guéneau, Thomas van Strydonck, Amin Timany, Alix Trieu, Dominique Devriese, Lars Birkedal. Under submission.
This is an extended, pedagogical introduction to the methodology from previous works including our POPL'21 paper
[ Coq development | pdf ]

Published articles

Proving Full-System Security Properties under Multiple Attacker Models on Capability Machines, Thomas van Strydonck, Aïna Linn Georges, Armaël Guéneau, Alix Trieu, Amin Timany, Frank Piessens, Lars Birkedal, Dominique Devriese. CSF'22.
[ bib | pdf ]

Theorems for Free from Separation Logic Specifications, Lars Birkedal, Thomas Dinsdale-Young, Armaël Guéneau, Guilhem Jaber, Kasper Svendsen, Nikos Tzevelekos. ICFP 2021.
Recipient of ICFP 2021 Distinguished Paper Award.
[ bib | Coq development | Coq development (artifact) | pdf | video ]

Cap’ ou pas cap’ ? Preuve de programmes pour une machine à capacités en presence de code inconnu, or Program verification on a capability machine in presence of untrusted code. 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 | pdf (english version) | slides ]

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 ]

Misc

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 ]