Chris Hawblitzel
where else to find them
no profile links on file
what they talk about
all 6 in the filters
where they keep going back
- OOPSLA2 editions2022–2023
all 8 in the filters
on a stage with
all 53 in the filters
who talks about the same things
- Travis Hance7 talks
- Exequiel Rivas6 talks
- Bryan Parno22 talks
- Cătălin Hriţcu16 talks
- Karthikeyan Bhargavan5 talks
- Jon Howell8 talks
| title | conference | date |
|---|---|---|
| Project Everest: Perspectives from Developing Industrial-Grade High-Assurance(…) | PLDI 2026 | 2026-06-15 |
Project Everest produces a verified TLS stack and crypto suite rather than promises: it yields 1.3 million lines of F source that build in two hours, emits… | ||
| Tunable Automation in Automated Program Verification | Dafny 2026 | 2026-01-11 |
A Rust-based verifier (Verus) adds a broadcast lemmas mechanism to let libraries export grouped, universally quantified facts and users import them at module… | ||
| PoWER Never Corrupts: Tool-Agnostic Verification of Crash Consistency and Corruption... | OSDI '25 | 2025-07-07 |
Claims tool-agnostic verification of crash consistency via PoWER (Preconditions on Writes Enforcing Recoverability), implements an explicit model of media… | ||
| VeriSMo: A Verified Security Module for Confidential VMs | 18th USENIX Symposium on Operating Systems Design and Implementation (OSDI '24) | 2024-07-10 |
VERISMO implements a Rust security module for AMD SEV-SNP that is formally verified for functional correctness, secure information flow, and VM confidentiality… | ||
| Verus: Verifying Rust Programs using Linear Ghost Types | OOPSLA 2023 | 2023-10-23 |
Verus is an SMT-based verifier that embeds proofs in Rust and uses linear ghost permissions to represent ownership-aligned memory permissions; the tool demands… | ||
| Sharding the State Machine: Automated Modular Reasoning for Complex Concurrent System | OSDI 2023 | 2023-07-10 |
IronSync is an automated verification framework that uses an ownership type system and a Localized Transition System to split global proofs into small… | ||
| Linear types for large-scale systems verification | OOPSLA 2022 | 2022-12-05 |
Integrates linear Dafny with Dafny's SMT backend to push memory reasoning into the type system while keeping SMT for heap invariants; implements… | ||
| Vale: Verifying High-Performance Cryptographic Assembly Code | 26th USENIX Security Symposium (USENIX Security '17) | 2017-08-16 |
Vale converts annotated, hand-tuned assembly into an abstract syntax tree and emits machine-checked proofs verified by an SMT-based verifier, letting the AST… | ||
| Cosh: Clear OS Data Sharing In An Incoherent World | TRIOS ’14 | 2014-10-05 |
Cosh: Clear OS Data Sharing In An Incoherent World
Andrew Baumann, and Chris Hawblitzel, Microsoft Research; Kornilios Kourtis, ETH Zürich; Tim Harris, Oracle… | ||
| nothing matches | ||