Peter W. O'Hearn
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–2024
all 7 in the filters
on a stage with
all 11 in the filters
who talks about the same things
- Peter Müller28 talks
- Thibault Dardinier9 talks
- Noam Zilberstein6 talks
- Simon Oddershede Gregersen9 talks
- Benjamin Lucien Kaminski14 talks
- Rupak Majumdar21 talks
| title | conference | date |
|---|---|---|
| Non-Termination Proving at Scale | OOPSLA 2024 | 2024-10-20 |
Claims a sound and complete under-approximate logic called UNTerSL that composes incorrectness/divergence reasoning with separation logic and bi-abduction to… | ||
| AI for the People | N40AI 2024 | 2024-01-20 |
Built an incremental Infer-based analyzer that runs on code changes against 100,000 commits per week, comments on pull requests and shifts fix rate from… | ||
| My Journey to the Dark Side: Under-Approximation, Incorrectness, Proof | Incorrectness 2024 | 2024-01-17 |
Talk describes concrete methods and outcomes: an analyzer built with an abstract interpreter and abduction summaries runs in CI, finds 25,000 race bugs in a… | ||
| Finding real bugs in big programs with incorrectness logic | OOPSLA 2022 | 2022-12-05 |
Pulse-X applies ISL (a synthesis of Incorrectness Logic and separation logic) to build an automatic under-approximate analyzer for memory errors, inferring… | ||
| Applying Formal Verification to Microkernel IPC at Meta | CPP 2022 | 2022-01-17 |
Project uses Iris in Coq to verify the microkernel IPC algorithms (not the full C), proving correctness of two queues verified implemented as non‑blocking… | ||
| Concurrent Incorrectness Separation Logic | POPL 2022 | 2022-01-16 |
Develops CISL as a parametric extension of Incorrectness Separation Logic that models concurrency with histories and lock-aware events, instantiates to race… | ||
| SOAP - Keynote: Formal Reasoning and the Hacker Way | SOAP 2020 | 2020-06-15 |
A compositional static analyzer called Infer is wired into CI to run on diffs rather than nightly batches, and this deployment change raises developer fix rate… | ||
| Ask Me Anything with Peter O'Hearn | PLDI 2020 | 2020-06-15 |
Answers claim a shift from heavy upfront specs to a pay-as-you-go model where small specs give incremental value, and point to concrete tools: Infer team work… | ||
| nothing matches | ||