Bryan Parno
where else to find them
github:parno
what they talk about
all 9 in the filters
where they keep going back
- OOPSLA4 editions2022–2025
all 13 in the filters
on a stage with
all 74 in the filters
who talks about the same things
- Jay Bosamiya6 talks
- Conrad Watt12 talks
- Jean Pichon-Pharabod12 talks
- Marco Patrignani14 talks
- Craig Disselkoen4 talks
- Philippa Gardner17 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… | ||
| Scaling Instruction-Selection Verification against Authoritative ISA Semantics | OOPSLA 2025 | 2025-10-16 |
Arrival verifies Cranelift instruction selection end to end by composing rules (rule chaining) and auto‑deriving ISA specs from vendor ASL via a… | ||
| OwlC: Compiling Security Protocols to Verified, Secure... | USENIX Security '25 | 2025-08-13 |
OwlC compiles Owl protocol specifications into side‑channel‑resistant Rust libraries and mechanically verifies their fidelity to an itrees specification using… | ||
| TRex: Practical Type Reconstruction for Binary Code | USENIX Security '25 | 2025-08-13 |
TRex is a deductive constraint-based tool that reconstructs behavior-capturing types using structural types and a final type rounding step, producing pointers… | ||
| Vest: Verified, Secure, High-Performance Parsing and Serialization for Rust | USENIX Security '25 | 2025-08-13 |
Vest generates Rust zero-copy parsers and in-place serializers from an RFC-like DSL, proves memory safety plus soundness, completeness, non-malleability and… | ||
| Basilisk: Using Provenance Invariants to Automate Proofs of Undecidable Protocols | OSDI '25 | 2025-07-07 |
Basilisk is a Daphne compiler extension that automatically derives inductive invariants for distributed protocols using Provenance Invariants and an analysis… | ||
| Keynote: Bringing Verified Cryptographic Protocols to Practice | PriSC 2025 (with POPL 2025) | 2025-01-20 |
A toolchain produces provably secure, interoperable protocol implementations: a type-based verifier Owl yields computationally sound proofs, an SMT-backed… | ||
| Towards Proof Stability in SMT-based Program Verification | Dafny 2025 | 2025-01-19 |
Paper and prototype work presents a mutation-driven detector Mariposa mutation-based detector and an SMT-level pruning algorithm that use Z3 proof-of-unsat and… | ||
| Teaching Types and Non-Interference in Dafny | Dafny 2025 | 2025-01-19 |
Teaching Types and Non-Interference in Dafny (Video, Dafny 2025)
Bryan Parno
(Carnegie Mellon University)
Abstract: We relate our approach to teaching a unit… | ||
| FlowCert: Translation Validation for Asynchronous Dataflow Programs via Dynamic(…) | OOPSLA 2024 | 2024-10-20 |
FlowCert implements translation validation from LLVM to asynchronous dataflow graphs for the RipTide CGRA by constructing a deterministic canonical schedule… | ||
| Inductive Invariants That Spark Joy: Using Invariant Taxonomies to Streamline... | 18th USENIX Symposium on Operating Systems Design and Implementation (OSDI '24) | 2024-07-10 |
Claim: Kondo auto-generates and proves the network-level lemmas that make host-level invariants inductive, so developers only prove the synchronous proof about… | ||
| 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… | ||
| Leaf: Modularity for Temporary Sharing in Separation Logic | OOPSLA 2023 | 2023-10-23 |
Claims a single abstraction that encodes temporary read sharing across different permission systems and shows it works concretely: a guarding operator that… | ||
| 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… | ||
| FastVer2: A Provably Correct Monitor for Concurrent, Key-Value Stores | CPP 2023 | 2023-01-16 |
FastVer2 is a verified, concurrent monitor for the Faster key-value store: implemented in C (≈8,000 lines produced from ≈50,000 lines of F proofs) using the… | ||
| MSWasm: Soundly Enforcing Memory-Safe Execution of Unsafe Code | POPL 2023 | 2023-01-15 |
Extends Wasm with segmented memory and unforgeable handles that carry colored provenance, a formal semantics, and a proof that well-typed MSWasm modules are… | ||
| 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… | ||
| Finding Invariants of Distributed Systems: It's a Small (Enough) World After All | NSDI ’21 | 2021-04-12 |
Swiss automates construction of inductive invariants by exhaustively searching a bounded candidate space, using counterexample-guided synthesis and SMT checks… | ||
| Don't Yank My Chain: Auditable NF Service Chaining | NSDI ’21 | 2021-04-12 |
AuditBox is a deployed system that uses trusted execution environments (Intel SGX enclaves) plus a per-NF verification shim to produce continuous, provable… | ||
| 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… | ||
| Embassies: Radically Refactoring the Web | NSDI 2013 | 2013-04-02 |
Argues for replacing the browser’s sprawling API with a tiny, well-specified client execution interface that runs vendor-supplied native code in per-site… | ||
| nothing matches | ||