Armaël Guéneau

14 papers A 3B 2Journal 8
YearRankTypeTitle / Venue / Authors
2026 B conf
Using Ghost Ownership to Verify Union-Find and Persistent Arrays in Rust.
CPP
Arnaud Golfouse, Armaël Guéneau, Jacques-Henri Jourdan
2025 J jnl
Verified Purely Functional Catenable Real-Time Deques.
CoRR
Jules Viennot, Arthur Wendling, Armaël Guéneau, François Pottier
2024 J jnl
Cerise: Program Verification on a Capability Machine in the Presence of Untrusted Code.
J. ACM
Aïna Linn Georges, Armaël Guéneau, Thomas Van Strydonck, Amin Timany, Alix Trieu, Dominique Devriese, Lars Birkedal
2024 J jnl
The Logical Essence of Well-Bracketed Control Flow.
Proc. ACM Program. Lang.
Amin Timany, Armaël Guéneau, Lars Birkedal
2024 J jnl
Thunks and Debits in Separation Logic with Time Credits.
Proc. ACM Program. Lang.
François Pottier, Armaël Guéneau, Jacques-Henri Jourdan, Glen Mével
2023 J jnl
Melocoton: A Program Logic for Verified Interoperability Between OCaml and C.
Proc. ACM Program. Lang.
Armaël Guéneau, Johannes Hostert, Simon Spies, Michael Sammler, Lars Birkedal, Derek Dreyer
2022 A conf
Proving full-system security properties under multiple attacker models on capability machines.
CSF
Thomas Van Strydonck, Aïna Linn Georges, Armaël Guéneau, Alix Trieu, Amin Timany, Frank Piessens, Lars Birkedal, Dominique Devriese
2021 J jnl
Efficient and provable local capability revocation using uninitialized capabilities.
Proc. ACM Program. Lang.
Aïna Linn Georges, Armaël Guéneau, Thomas Van Strydonck, Amin Timany, Alix Trieu, Sander Huyghebaert, Dominique Devriese, Lars Birkedal
2021 J jnl
Theorems for free from separation logic specifications.
Proc. ACM Program. Lang.
Lars Birkedal, Thomas Dinsdale-Young, Armaël Guéneau, Guilhem Jaber, Kasper Svendsen, Nikos Tzevelekos
2019 B conf
Formal Proof and Analysis of an Incremental Cycle Detection Algorithm.
ITP
Armaël Guéneau, Jacques-Henri Jourdan, Arthur Charguéraud, François Pottier
2019 — —
Mechanized Verification of the Correctness and Asymptotic Complexity of Programs. (Vérification mécanisée de la correction et complexité asymptotique de programmes).
Armaël Guéneau
2018 A conf
A Fistful of Dollars: Formalizing Asymptotic Complexity Claims via Deductive Program Verification.
ESOP
Armaël Guéneau, Arthur Charguéraud, François Pottier
2017 A conf
Verified Characteristic Formulae for CakeML.
ESOP
Armaël Guéneau, Magnus O. Myreen, Ramana Kumar, Michael Norrish
2013 J jnl
The ins and outs of iteration in Mezzo.
CoRR
Armaël Guéneau, François Pottier, Jonathan Protzenko