Kenneth L. McMillan
where else to find them
no profile links on file
what they talk about
where they keep going back
no series more than once — all 4 in the filters
on a stage with
all 12 in the filters
who talks about the same things
- Oded Padon11 talks
- Sharon Shoham13 talks
- Jon Howell8 talks
- James R. Wilcox4 talks
- Mooly Sagiv18 talks
- Neta Elad3 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… | ||
| 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… | ||
| Synthesizing History and Prophecy Variables for Symbolic Model Checking | VMCAI 2023 | 2023-01-15 |
Presents an automated CEGAR pipeline that introduces prophecy and history variables to remove universal quantifiers over arrays, using counterexample-guided… | ||
| 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 | ||