Aneris: A Mechanised Logic for Modular Reasoning about Distributed Systems

DOI10.1007/978-3-030-44914-8_13OpenAlexW3016987934MaRDI QIDQ5041100

Amin Timany, Marit Edna Ohlenbusch, Morten Krogh-Jespersen, Simon Oddershede Gregersen, Lars Birkedal

Publication date: 13 October 2022

Published in: Programming Languages and Systems (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-030-44914-8_13

zbMATH Keywords

distributed systemsformal verificationhigher-order logicconcurrencyseparation logic

Mathematics Subject Classification ID

Logic in computer science (03B70) Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Related Items (2)

Why3-do: the way of harmonious distributed system proofs ⋮ Protocol combinators for modeling, testing, and execution of distributed systems

Uses Software

• SPIN
• Verdi
• Chapar
• Rust
• RustBelt

Cites Work

• Unnamed Item
• Resources, concurrency, and local reasoning
• Operating systems. An advanced course
• Iris
• Chapar: certified causally consistent distributed key-value stores
• Views
• Subjective auxiliary state for coarse-grained concurrency
• Higher-order ghost state
• The Essence of Higher-Order Concurrent Separation Logic
• Dafny: An Automatic Program Verifier for Functional Correctness
• Multiparty asynchronous session types
• Proving the Correctness of Multiprocess Programs
• Iris from the ground up: A modular foundation for higher-order concurrent separation logic
• Unifying refinement and hoare-style reasoning in a logic for higher-order concurrency
• Interactive proofs in higher-order concurrent separation logic
• Dynamic multirole session types
• Impredicative Concurrent Abstract Predicates
• Communicating State Transition Systems for Fine-Grained Concurrent Resources

This page was built for publication: Aneris: A Mechanised Logic for Modular Reasoning about Distributed Systems