Aina Linn Georges
where else to find them
what they talk about
all 6 in the filters
where they keep going back
all 7 in the filters
on a stage with
all 31 in the filters
who talks about the same things
- Jean Pichon-Pharabod12 talks
- Maxime Legoupil5 talks
- June Rousseau2 talks
- Conrad Watt12 talks
- Philippa Gardner17 talks
- Xiaojia Rao3 talks
| title | conference | date |
|---|---|---|
| Endangered by the Language But Saved by the Compiler: Robust Safety via Semantic(…) | POPL 2026 | 2026-01-11 |
Shows a hardening compiler that makes a C‑like source (Rec) robustly safe only after compilation to a CHERI‑style capability machine (Cap); proves a separation… | ||
| A Semantic Approach to Robust Property Preservation | PriSC 2025 (with POPL 2025) | 2025-01-20 |
Proposes a semantic reduction of robust property preservation: replace hard syntactic backtranslation with a backtranslation between semantic domains, so… | ||
| The Nextgen Modality: A Modality for Non-Frame-Preserving Updates in Separation Logic | CPP 2025 | 2025-01-20 |
Proposes a new modality that permits non-frame-preserving updates to ghost state inside Iris, formalizes a parameterized stack-cutting transformation that… | ||
| Data Race Freedom à la Mode | POPL 2025 | 2025-01-19 |
DRFcaml extends OCaml's type system with new mode axes (contention and portability) to statically guarantee data-race freedom for multi-threaded OCaml while… | ||
| Iris-MSWasm: elucidating and mechanising the security invariants of Memory-Safe(…) | OOPSLA 2024 | 2024-10-20 |
Mechanisation produces MSWasmCert as a conservative, proof‑assistant formalisation of MSWasm and WebAssembly 1.0 modules, and builds Iris‑MSWasm: a separation… | ||
| Proving capability safety in the presence of indirect sentries | POCL 2024 | 2024-01-16 |
Extends a CHERI-style miniature machine (SeRiES) with indirect sentries, adapts an Iris-like program logic plus a new logical relation, and produces… | ||
| Iris-Wasm: Robust and Modular Verification of WebAssembly Programs | PLDI 2023 | 2023-06-17 |
Iris-Wasm mechanizes Wasm 1.0 in Coq on top of the Iris framework and claims modular, higher-order verification that composes across host boundaries. It builds… | ||
| SECOMP2CHERI: Securely Compiling Compartments from CompCert C to a Capability M... | PriSC 2023 | 2023-01-21 |
Extension of CompCert implements CompCert with compartments that enforces interfaces, disables cross-compartment inlining/tailcalls, and updates Coq… | ||
| Le Temps des Cerises: Efficient Temporal Stack Safety on Capability Machines using Directed | OOPSLA 2022 | 2022-12-05 |
Introduces directed capabilities that add one extra bit and a single arithmetic bounds check to CHERI-style machines, enabling a calling convention that… | ||
| Efficient, Provable Local Capability Revocation using Uninitialized Capabilities | POPL 2021 | 2021-01-17 |
Proposes uninitialized capabilities that give write-only access to an uninitialized stack region and require overwriting before any read, implemented with… | ||
| Implementing a Capability Machine Model into Iris | PriSC 2020 | 2020-01-25 |
Mechanization of a core capability-machine model into Iris, with an embedding of a machine language and a mechanized logical relation that solves the world… | ||
| nothing matches | ||