Jon Howell
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 5 in the filters
on a stage with
all 31 in the filters
who talks about the same things
- Kenneth L. McMillan4 talks
- Sharon Shoham13 talks
- Travis Hance7 talks
- Oded Padon11 talks
- Mooly Sagiv18 talks
- Peter Müller28 talks
| title | conference | date |
|---|---|---|
| Anvil: Verifying Liveness of Cluster Management Controllers | 18th USENIX Symposium on Operating Systems Design and Implementation (OSDI '24) | 2024-07-10 |
Anvil presents eventually stable reconciliation as a concise temporal liveness spec and provides a Rust framework that verifies controllers against it using… | ||
| Domesticating Automation | Dafny 2024 | 2024-01-14 |
Proposes a module-granular view of the quantifier instantiation graph and a crude metric that ranks modules by how many downstream instantiations they enable… | ||
| 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… | ||
| Counterexample Driven Quantifier Instantiations with Applications to Distribute... | OOPSLA 2023 | 2023-10-23 |
Replaces problematic function symbols with a one-to-one relational abstraction inside Ivy and drives refinements by solver counterexamples; SMT solvers that… | ||
| 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… | ||
| 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… | ||
| 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 | ||