David Swasey
where else to find them
what they talk about
where they keep going back
no series more than once — all 3 in the filters
on a stage with
all 4 in the filters
who talks about the same things
nobody close enough yet
| title | conference | date |
|---|---|---|
| Verification of Templated Code in C++ | RocqPL 2026 | 2026-01-17 |
Claims a method to verify C++ templates without expanding the trusted computing base by treating unresolved symbols as hygienic macros and using a shallowly… | ||
| Towards Modular Specification and Verification of Concurrent Hypervisor-based I... | PriSC 2024 | 2024-01-20 |
NOVA is a microhypervisor of 17K lines and 15 hypercalls whose specification (~100 pages) is decomposed with Iris-based separation logic into WP_Nova_EC and… | ||
| A Case for Lightweight Interfaces in Coq | CoqPL 2022 | 2022-01-22 |
Bedrock uses Coq and the Iris program logic to verify a large concurrent C++ hypervisor stack and finds Coq’s lack of lightweight interface files hurts scale… | ||
| nothing matches | ||