Martin Avanzini
where else to find them
what they talk about
where they keep going back
- OOPSLA2 editions2020–2024
on a stage with
all 6 in the filters
who talks about the same things
- Georg Moser5 talks
- Benjamin Gregoire6 talks
- Gilles Barthe17 talks
- Gabriele Vanoni7 talks
- Michael Schaper2 talks
- Benjamin Lucien Kaminski14 talks
| title | conference | date |
|---|---|---|
| A quantitative probabilistic relational Hoare logic | POPL 2025 | 2025-01-19 |
eRHL is a program logic whose pre/post-conditions are nonnegative real-valued functions on pairs of states, and it gives upper bounds on expectations… | ||
| Hopping Proofs of Expectation-Based Properties: Applications to Skiplists and Security(…) | OOPSLA 2024 | 2024-10-20 |
Proposes a EHL + pRHL hopping rule that reduces expectation-based proof goals to related programs, implements it inside EasyCrypt integration, and proves… | ||
| Automated Expected Value Analysis of Recursive Programs | PLDI 2023 | 2023-06-17 |
Defines infer[.], a term representation that translates weakest pre-expectation semantics for recursive, imperative probabilistic programs into first-order… | ||
| A Modular Cost Analysis for Probabilistic Programs | OOPSLA 2020 | 2020-11-15 |
Presents a modular method that derives symbolic upper bounds on expected resource cost for probabilistic imperative programs by combining the ERT-calculus with… | ||
| nothing matches | ||