Travis Hance
where else to find them
what they talk about
all 4 in the filters
where they keep going back
no series more than once — all 6 in the filters
on a stage with
all 26 in the filters
who talks about the same things
- Chris Hawblitzel9 talks
- Laila Elbeheiry4 talks
- Ranjit Jhala19 talks
- Jon Howell8 talks
- Derek Dreyer35 talks
- Peter Müller28 talks
| title | conference | date |
|---|---|---|
| VerusBelt: A Semantic Foundation for Verus’s Proof-Oriented Extensions to the Rust Type(…) | PLDI 2026 | 2026-06-15 |
Paper proves a machine-checked soundness theorem for a Verus subset by formalizing Verus’s proof-oriented types and translating them into Rust Hornbill–style… | ||
| 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… | ||
| 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… | ||
| Liquid Information Flow Control | ICFP 2020 | 2020-08-23 |
Claims a new DSL called Lifty domain-specific language that encodes information-flow policies as liquid refinements and enforces them with a TIO-style security… | ||
| nothing matches | ||