Hoang-Hai Dang
where else to find them
no profile links on file
what they talk about
where they keep going back
no series more than once — all 3 in the filters
on a stage with
all 12 in the filters
who talks about the same things
- Lennard Gäher7 talks
- Michael Sammler16 talks
- Jeehoon Kang14 talks
- Derek Dreyer35 talks
- Simon Spies8 talks
- Ralf Jung18 talks
| title | conference | date |
|---|---|---|
| Specifying and Verifying the NOVA Microhypervisor in Concurrent Separation Logic | RocqPL 2026 | 2026-01-17 |
Verification of the NOVA microhypervisor uses BRiCk C++ program logic built on Iris and Skylabs proof automation to prove concurrency properties of about… | ||
| Modularizing CPU Semantics for Virtualization | PriSC 2024 | 2024-01-20 |
Proposes a concrete decomposition of ARM ASL into an unprivileged core and a small privileged handler so one common unprivileged semantics can be reused across… | ||
| 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… | ||
| Simuliris: A Separation Logic Framework for Verifying Concurrent Program Optimiz | POPL 2022 | 2022-01-16 |
Framework claims a mechanically checked simulation that preserves contextual refinement and termination under a fair scheduler for real concurrent compiler… | ||
| nothing matches | ||