Aleksandar Nanevski
where else to find them
what they talk about
all 4 in the filters
where they keep going back
- POPL2 editions2021–2022
all 4 in the filters
on a stage with
- Adam Morrisononce
- Alexander Gryzlovonce
- Anindya Banerjeeonce
all 13 in the filters
who talks about the same things
- Anindya Banerjee5 talks
- Germán Andrés Delbianco4 talks
- Ignacio Fábregas3 talks
- Michael Sammler16 talks
- Amin Timany16 talks
- Simon Spies8 talks
| title | conference | date |
|---|---|---|
| Verifying Graph Algorithms in Separation Logic: A Case for an Algebraic Approach | ICFP 2025 | 2025-10-12 |
Graphs become a partial commutative monoid so they support join-based decomposition; structure-preserving PCM morphisms distribute over joins and let proofs… | ||
| Visibility Reasoning for Concurrent Snapshot Algorithms | POPL 2022 | 2022-01-16 |
Applies visibility relations to prove linearizability for three Jayanti algorithms, giving a reusable, layered proof instead of locating linearization points… | ||
| On Algebraic Abstractions for Concurrent Separation Logics | POPL 2021 | 2021-01-17 |
Defines morphisms of PCMs and separating relations as the concrete algebraic machinery that preserves ownership across parallel composition, then uses them to… | ||
| 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… | ||
| How to make ad hoc proof automation less ad hoc | Lambda World Cádiz 2018 | 2018-10-25 |
Coq proof automation becomes an instance of ad hoc polymorphism: dependent overloaded theorem records encode both a heap shape and a proof, and Coq’s… | ||
| nothing matches | ||