Armaël Guéneau

According to our database, Armaël Guéneau authored at least 16 papers between 2013 and 2024.

Collaborative distances:

• Dijkstra number of four.
• Erdős number of four.

2024

The Logical Essence of Well-Bracketed Control Flow.

Amin Timany, Armaël Guéneau, Lars Birkedal

Proc. ACM Program. Lang., January, 2024

Thunks and Debits in Separation Logic with Time Credits.

François Pottier, Armaël Guéneau, Jacques-Henri Jourdan, Glen Mével

Proc. ACM Program. Lang., January, 2024

Cerise: Program Verification on a Capability Machine in the Presence of Untrusted Code.

Aïna Linn Georges, Armaël Guéneau, Thomas Van Strydonck, Amin Timany, Alix Trieu, Dominique Devriese, Lars Birkedal

J. ACM, 2024

2023

The Logical Essence of Well-Bracketed Control Flow (Artifact).

Amin Timany, Armaël Guéneau, Lars Birkedal

Dataset, November, 2023

The Logical Essence of Well-Bracketed Control Flow (Artifact).

Amin Timany, Armaël Guéneau, Lars Birkedal

Dataset, November, 2023

The Logical Essence of Well-Bracketed Control Flow (Artifact).

Amin Timany, Armaël Guéneau, Lars Birkedal

Dataset, November, 2023

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

Proc. ACM Program. Lang., October, 2023

2022

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

Proceedings of the 35th IEEE Computer Security Foundations Symposium, 2022

2021

Proving full-system security properties under multiple attacker models on capability machines: Coq mechanization.

Thomas Van Strydonck, Aïna Linn Georges, Armaël Guéneau, Alix Trieu, Amin Timany, Frank Piessens, Lars Birkedal, Dominique Devriese

Dataset, September, 2021

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, Lars Birkedal

Proc. ACM Program. Lang., 2021

Theorems for free from separation logic specifications.

Lars Birkedal, Thomas Dinsdale-Young, Armaël Guéneau, Guilhem Jaber, Kasper Svendsen, Nikos Tzevelekos

Proc. ACM Program. Lang., 2021

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

PhD thesis, 2019

Formal Proof and Analysis of an Incremental Cycle Detection Algorithm.

Armaël Guéneau, Jacques-Henri Jourdan, Arthur Charguéraud, François Pottier

Proceedings of the 10th International Conference on Interactive Theorem Proving, 2019

2018

A Fistful of Dollars: Formalizing Asymptotic Complexity Claims via Deductive Program Verification.

Armaël Guéneau, Arthur Charguéraud, François Pottier

Proceedings of the Programming Languages and Systems, 2018

2017

Verified Characteristic Formulae for CakeML.

Armaël Guéneau, Magnus O. Myreen, Ramana Kumar, Michael Norrish

Proceedings of the Programming Languages and Systems, 2017

2013

The ins and outs of iteration in Mezzo.

Armaël Guéneau, François Pottier, Jonathan Protzenko

CoRR, 2013