Conrad Watt
where else to find them
what they talk about
all 4 in the filters
where they keep going back
- POPL3 editions2022–2025
- PLDI Workshop Honoring Andreas Podelski2 editions2023–2024
all 5 in the filters
on a stage with
all 42 in the filters
who talks about the same things
- Jean Pichon-Pharabod12 talks
- Andreas Rossberg13 talks
- Xiaojia Rao3 talks
- Philippa Gardner17 talks
- Bryan Parno22 talks
- Aina Linn Georges12 talks
| title | conference | date |
|---|---|---|
| Verification of WebAssembly Features | RPLS 2025 | 2025-06-17 |
A mechanized WebAssembly semantics exists in Isabelle mechanization and parallel mechanizations target Rock/MetaRoc, with proven preservation and progress for… | ||
| Lighting talks and closing discussion | WAW 2025 | 2025-01-20 |
spectTech starts from a dependently typed DSL that encodes WebAssembly plus annotations and already yields automated artifacts (LaTeX, an interpreter and… | ||
| Generically Automating Separation Logic by Functors, Homomorphisms, and Modules | POPL 2025 | 2025-01-19 |
Claims a generic theory that generates separation logic reasoning rules from algebraic signatures (functors, homomorphisms, modules) and a compositional… | ||
| Progressful Interpreters for Efficient WebAssembly Mechanisation | POPL 2025 | 2025-01-19 |
Implements a progressful interpreter in Coq that uses dependent types to certify both soundness and progress, and extracts an executable with proofs erasable… | ||
| Bringing the WebAssembly Standard up to Speed with SpecTec | PLDI 2024 | 2024-06-24 |
SpecTec is a DSL and toolchain that serves as a single source of truth for Wasm semantics, generating typeset spec prose, formal definitions, and a meta-level… | ||
| Panel Discussion: Browsers & Wasm | WasmCon 2023 | 2023-09-06 |
Browsers report concrete work: baseline compilers like liftoff and Mozilla’s BBQ compile quickly while OMG/TurboFan and Balder optimize later, and V8 runs a… | ||
| WasmRef-Isabelle: A Verified Monadic Interpreter and Industrial Fuzzing Oracle for(…) | PLDI 2023 | 2023-06-17 |
A verified monadic interpreter for WebAssembly implemented in Isabelle/HOL and proven via a two-step refinement proof against WasmCert-Isabelle, extracted to… | ||
| 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… | ||
| MSWasm: Soundly Enforcing Memory-Safe Execution of Unsafe Code | POPL 2023 | 2023-01-15 |
Extends Wasm with segmented memory and unforgeable handles that carry colored provenance, a formal semantics, and a proof that well-typed MSWasm modules are… | ||
| Isolation without Taxation: Near-Zero-Cost Transitions for WebAssembly and SFI | POPL 2022 | 2022-01-16 |
Paper claims that adding static invariants lets sandboxed code use simple function calls instead of heavyweight wrappers, and implements this end-to-end. A… | ||
| nothing matches | ||