Roberto Guanciale
where else to find them
what they talk about
where they keep going back
- OOPSLA2 editions2023–2024
on a stage with
- Mads Dam2×
- Alceste Scalasonce
- Andreas Lindneronce
all 14 in the filters
who talks about the same things
- Alceste Scalas5 talks
- Nate Foster24 talks
- Eric Hayden Campbell6 talks
- Philipp Haller11 talks
- David Walker15 talks
- Tobias Kappé4 talks
| title | conference | date |
|---|---|---|
| Towards Verifiable System Code using a DSL Compiled to Efficient and Readable C Code | LCTES 2026 | 2026-06-15 |
A minimal, purely functional DSL called Barocq compiles via Rocq to readable C by enforcing a strict alias-control discipline so the compiler does zero-cost… | ||
| Forward Symbolic Execution for Trustworthy Automation of Binary Code Verification | VMCAI 2026 | 2026-01-12 |
A sound, proof-producing symbolic execution framework is formalized and implemented in HOL4 theorem prover and HolBA, instantiated for the BIR intermediate… | ||
| HOL4P4: mechanized small-step semantics for P4 | OOPSLA 2024 | 2024-10-20 |
Claims a first complete P416 semantics that models extern-concurrency interactions and captures pipelines end-to-end, formalized in HOL4 with a heapless… | ||
| P4R-Type: A Verified API for P4 Control Plane Programs | OOPSLA 2023 | 2023-10-23 |
Library implements a verified Scala API that encodes P4Info as Scala types and statically rejects mismatches between P4 tables, allowed actions, and action… | ||
| nothing matches | ||