Oded Padon
where else to find them
what they talk about
all 7 in the filters
where they keep going back
all 6 in the filters
on a stage with
all 39 in the filters
who talks about the same things
- Sharon Shoham13 talks
- Kenneth L. McMillan4 talks
- Neta Elad3 talks
- Mooly Sagiv18 talks
- Michael Sammler16 talks
- Takeshi Tsukada16 talks
| title | conference | date |
|---|---|---|
| Simplifying Safety Proofs with Forward-Backward Reasoning and Prophecy | PLDI 2026 | 2026-06-15 |
Proposes a proof system that breaks a single complex inductive invariant into incremental steps and proves each rule sound, implemented as a checker in myvy… | ||
| Mirage: A Multi-Level Superoptimizer for Tensor Programs | OSDI '25 | 2025-07-07 |
Mirage is a multi-level superoptimizer that generates custom CUDA kernels from tensor programs using a uniform representation across kernel, thread-block, and… | ||
| A Primal-Dual Perspective on Program Verification Algorithms | POPL 2025 | 2025-01-19 |
Presents a unified algorithmic framework that generalizes Lagrangians to discrete domains (powersets, predicates, ranking functions) and runs an abstract… | ||
| Quarl: A Learning-Based Quantum Circuit Optimizer | OOPSLA 2024 | 2024-10-20 |
Quarl is a reinforcement-learning quantum circuit optimizer that replaces greedy search with a policy trained via PPO, decomposes millions of actions into a… | ||
| 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… | ||
| An Infinite Needle in a Finite Haystack: Finding Infinite Counter-Models in Dedu... | POPL 2024 | 2024-01-14 |
Proposes a finite, machine-checkable representation of certain infinite first-order models called symbolic structures and encodes model checking into linear… | ||
| 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… | ||
| CLOVER: Closed-Loop Verifiable Code Generation | Dafny 2024 | 2024-01-14 |
Generates code, docstrings, and formal annotations with GPT‑4 then applies six directed consistency checks (using reconstruction testing and the Dafny… | ||
| 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… | ||
| Induction Duality: Primal-Dual Search for Invariants | POPL 2022 | 2022-01-16 |
Presents a formal induction duality linking execution traces and bounded incremental proofs, and derives primal-dual Houdini, a symmetric algorithm that… | ||
| nothing matches | ||