Some Counterexamples for Compatible Triangulations. - Cody Barnson; Dawn Chandler; Qiao Chen; Christina Chung; Andrew Coccimiglio; Sean La; Lily Li; Aïna Linn; Anna Lubiw; Clare Lyle; Shikha Mahajan; Gregory W. Mierzwinski; et al. (CoRR, 2016)

LINCX: A Linear Logical Framework with First-Class Contexts. - Aïna Linn Georges; Agata Murawska; Shawn Otis; Brigitte Pientka (ESOP, 2017)

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)

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 (Zenodo, 2021)

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, 2022)

Le temps des cerises: efficient temporal stack safety on capability machines using directed capabilities. - Aïna Linn Georges; Alix Trieu; Lars Birkedal (Proc. ACM Program. Lang., 2022)

Le Temps des Cerises: Efficient Temporal Stack Safety on Capability Machines using Directed Capabilities (Artifact). - Aïna Linn Georges; Alix Trieu; Lars Birkedal (Zenodo, 2022)

Iris-Wasm: Robust and Modular Verification of WebAssembly Programs. - Xiaojia Rao; Aïna Linn Georges; Maxime Legoupil; Conrad Watt; Jean Pichon-Pharabod; Philippa Gardner; Lars Birkedal (Proc. ACM Program. Lang., 2023)

SECOMP: Formally Secure Compilation of Compartmentalized C Programs. - Jérémy Thibault; Roberto Blanco; Dongjae Lee; Sven Argo; Arthur Azevedo de Amorim; Aïna Linn Georges; Catalin Hritcu; Andrew Tolmach (CCS, 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)

Iris-MSWasm: Elucidating and Mechanising the Security Invariants of Memory-Safe WebAssembly. - Maxime Legoupil; June Rousseau; Aïna Linn Georges; Jean Pichon-Pharabod; Lars Birkedal (Proc. ACM Program. Lang., 2024)

Artifact and Appendix of 'Iris-MSWasm: elucidating and mechanising the security invariants of Memory-Safe WebAssembly'. - Maxime Legoupil; June Rousseau; Aïna Linn Georges; Jean Pichon-Pharabod; Lars Birkedal (Zenodo, 2024)

The Nextgen Modality: A Modality for Non-Frame-Preserving Updates in Separation Logic. - Simon Friis Vindum; Aïna Linn Georges; Lars Birkedal (CPP, 2025)

Data Race Freedom à la Mode. - Aïna Linn Georges; Benjamin Peters; Laila Elbeheiry; Leo White; Stephen Dolan; Richard A. Eisenberg; Chris Casinghino; François Pottier; Derek Dreyer (Proc. ACM Program. Lang., 2025)