Using the Prophecy-Based Encoding of Rust Borrows in a Realistic Verification Tool. Under submission. [ pdf ]
The Logical Essence of Well-Bracketed Control Flow.
Amin Timany, Armaël Guéneau, Lars Birkedal.
POPL 2024.
[ pdf
| doi
| Coq development ]
Thunks and Debits in Separation Logic with Time Credits.
François Pottier and Armaël Guéneau and Jacques-Henri Jourdan and Glen Mével.
POPL 2024.
[ pdf
| doi
| Coq development ]
Melocoton: A Program Logic for Verified Interoperability Between OCaml and C.
Armaël Guéneau, Johannes Hostert, Simon Spies, Michael Sammler, Lars Birkedal, Derek Dreyer.
OOPSLA 2023.
[ pdf
| doi
| Coq development
| website ]
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.
Journal of the ACM, 2023.
This is an extended, pedagogical introduction to the methodology from previous works including our POPL'21 paper
[ Coq development
| pdf
| doi ]
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
| doi ]
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
| pdf
| doi
| 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
| doi ]
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
| doi
| 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
| doi
| 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
| doi
| slides ]
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 ]