Sharon Shoham
where else to find them
github:sharonsh
what they talk about
where they keep going back
all 4 in the filters
on a stage with
all 28 in the filters
who talks about the same things
- Oded Padon11 talks
- Mooly Sagiv18 talks
- Neta Elad3 talks
- Kenneth L. McMillan4 talks
- Takeshi Tsukada16 talks
- Yotam M. Y. Feldman6 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… | ||
| Separating the Wheat from the Chaff: Understanding (In-)Completeness of Proof(…) | POPL 2026 | 2026-01-11 |
Main claim: the common fold/unfold proof steps are sound and — for the quantifier‑free, theory‑free fragment — complete for a weaker semantics called Weak… | ||
| 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… | ||
| Axe 'Em: Eliminating Spurious States with Induction Axioms | POPL 2025 | 2025-01-19 |
First-order abstractions get refined into well-founded or finite-domain semantics by instantiating an induction axiom schema guided by finitely representable… | ||
| 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… | ||
| 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… | ||
| Towards a Theoretical Understanding of Property-Directed Reachability | VMCAI 2023 | 2023-01-15 |
Shows that the SAT queries used by property‑directed reachability are strictly stronger than plain inductiveness checks, proving IC3 cannot be implemented in… | ||
| Panel: Next 50 Years of POPL | POPL 2023 | 2023-01-15 |
Panel discussion surveys POPL's past and future with concrete examples and tensions: cites FlashFill and program synthesis, the 1976 abstract interpretation… | ||
| Property-Directed Reachability as Abstract Interpretation in the Monotone Theory | POPL 2022 | 2022-01-16 |
Claims that propositional PDR is an instance of abstract interpretation by defining Lambda-PDR (take all counterexample generalizations) and a logical abstract… | ||
| Solving Constrained Horn Clauses Modulo Algebraic Data Types and Recursive Funct | POPL 2022 | 2022-01-16 |
Presents an IC3/PDR-inspired solver called Racer that combines relationification, controlled unfolding of recursive definitions, and uninterpreted-function… | ||
| Learning the Boundary of Inductive Invariants | POPL 2021 | 2021-01-17 |
An interpolation-based invariant inference algorithm with model-based generalization (dropping literals) uses bounded model checking to implement membership… | ||
| Proving Highly-Concurrent Traversals Correct | OOPSLA 2020 | 2020-11-15 |
Paper proves that optimistic lock-free traversals are correct by reducing concurrent traversal correctness to sequential reasoning plus two concrete… | ||
| nothing matches | ||