Peter Sewell
where else to find them
no profile links on file
what they talk about
all 8 in the filters
where they keep going back
- POPL5 editions2022–2026
- PLDI Workshop Honoring Andreas Podelski2 editions2025–2026
all 7 in the filters
on a stage with
all 32 in the filters
who talks about the same things
- Kayvan Memarian6 talks
- Christopher Pulte4 talks
- Michael Sammler16 talks
- Neel Krishnaswami10 talks
- Derek Dreyer35 talks
- Lars Birkedal35 talks
| title | conference | date |
|---|---|---|
| Combining Agentic AI and Lightweight Formal Methods To Find Bugs in a Production(…) | PAgE 2026 | 2026-06-15 |
Combines the executable-spec framework for Android pKVM with an OpenAI Codex-based agent that writes ambient-C ghost code and tests, running for about one… | ||
| Code-Specify-Test-Debug-Prove: Flexibly Integrating Separation Logic Specification into(…) | PLDI 2026 | 2026-06-15 |
Integrates CN separation logic into runtime checks, unit and SMT-based random generator testing, and final machine-checked proofs, all on the real-world PKVM… | ||
| ArchSem: Reusable Rigorous Semantics of Relaxed Architectures | POPL 2026 | 2026-01-11 |
A reusable framework composes ISA pseudo-code from Sail with concurrency interpreters in Rock via a freemonad of 15 algebraic effects, ingesting the full ARM… | ||
| Production Language Specification - Requirements for Multiple Usages | RPLS 2025 | 2025-06-17 |
Argues that one meta-language cannot serve all needs and surveys concrete tooling: LATeX/OCaml/Isabelle/HOL backends from LEM, a domain‑specific Sale front end… | ||
| Morello-Cerise: A Proof of Strong Encapsulation for the Arm Morello Capability Hardware(…) | PLDI 2025 | 2025-06-16 |
Proves that an encapsulated C-style component running on Arm Morello maintains a mod-64 accumulator invariant against arbitrary untrusted code, by mechanising… | ||
| A CHERI C Memory Model for Verified Temporal Safety | CPP 2025 | 2025-01-20 |
Defines a CHERI C object memory model that implements a new PNVI-CHERI provenance scheme, encodes five revocation strategies, and plugs into the Cerberus… | ||
| Fulminate: Testing CN Separation-Logic Specifications in C | POPL 2025 | 2025-01-19 |
Fulminate translates CN separation-logic annotations into executable C checks that enforce ownership ghost state and explicit ownership transfer at runtime… | ||
| Keynote: Can we reason about the security of concurrent systems code? | PriSC 2024 | 2024-01-20 |
Goal is to verify Google’s PKVM hypervisor running on ARM, not just papers: ARM semantics is captured in 420,000 lines of ARM spec (Sail/ASL), the hypervisor… | ||
| Welcome | The Future of Weak Memory 2024 | 2024-01-15 |
Program opens by defining weak versus strong memory and lists concrete agenda items: empirical validation of memory persistency models, tooling for checking… | ||
| An Axiomatic Basis for Computer Programming on the Relaxed Arm-A Architecture: T... | POPL 2024 | 2024-01-14 |
Claims a new separation logic AxSL for the Arm‑A user‑mode axiomatic model that lets relaxed reads/writes transfer resources when they induce ordering… | ||
| CN: Verifying Systems C Code with Separation-Logic Refinement Types | POPL 2023 | 2023-01-15 |
CN is a separation-logic refinement type system for ISO C that uses a Cerberus translation to a core language, implements resource types as first-class… | ||
| VIP: Verifying Real-World C Idioms with Integer-Pointer Casts | POPL 2022 | 2022-01-16 |
Presents VIP, a memory-object model that proves compatible with PNVI while making integer→pointer casts verifiable by adding an explicit provenance-copying… | ||
| nothing matches | ||