Gregory Malecha
where else to find them
no profile links on file
what they talk about
all 4 in the filters
where they keep going back
no series more than once — all 3 in the filters
on a stage with
all 8 in the filters
who talks about the same things
nobody close enough yet
| 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… | ||
| 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… | ||
| Recursive Mutexes in Separation Logic | RocqPL 2026 | 2026-01-17 |
Develops a separation-logic specification for recursive mutex built on the Brick logic and derived from a lower-level logically-atomic spec, with a per-thread… | ||
| 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… | ||
| 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 | ||