Aneris: Higher-Order Distributed Separation Logic

Aneris is a logic for verifying safety properties of distributed programs with unreliable communication primitives (akin to UDP).

Aneris is built on top of Iris—a state of the art concurrent separation logic.

Publications

2023 ICFP, Verifying Reliable Network Components in a Distributed Separation Logic with Dependent Separation Protocols,: Léon Gondelman, Jonas Kastberg Hinrichsen, Mário Pereira, Amin Timany, and Lars Birkedal.
2023 ECOOP, Modular Verification of State-Based CRDTs in Separation Logic,: Abel Nieto, Arnaud Daby-Seesaram, Léon Gondelman, Amin Timany, and Lars Birkedal.
2022 OOPSLA, Modular Verification of Op-Based CRDTs in Separation Logic,: Abel Nieto, Léon Gondelman, Alban Reynaud, Amin Timany, and Lars Birkedal.
2021 POPL, Distributed Causal Memory: Modular Specification and Verification in Higher-Order Distributed Separation Logic,: Léon Gondelman, Simon Oddershede Gregersen, Abel Nieto, Amin Timany, and Lars Birkedal.
2020 ESOP, Aneris: A Mechanised Logic for Modular Reasoning about Distributed Systems,: Morten Krogh-Jespersen, Amin Timany, Marit Edna Ohlenbusch, Simon Oddershede Gregersen, and Lars Birkedal.