Why3-do: the way of harmonious distributed system proofs
From MaRDI portal
Publication:6166787
DOI10.1007/978-3-030-99336-8_5zbMath1528.68248OpenAlexW4226498372MaRDI QIDQ6166787
Cláudio Belo Lourenço, Jorge Sousa Pinto
Publication date: 3 August 2023
Published in: Programming Languages and Systems (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-030-99336-8_5
Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Software engineering and formal methods. 10th international conference, SEFM 2012, Thessaloniki, Greece, October 1--5, 2012. Proceedings
- The existence of refinement mappings
- A Framework for Certified Self-Stabilization
- Dafny: An Automatic Program Verifier for Functional Correctness
- Self-stabilizing systems in spite of distributed control
- An improved algorithm for decentralized extrema-finding in circular configurations of processes
- One Logic to Use Them All
- Aneris: A Mechanised Logic for Modular Reasoning about Distributed Systems
- Why3 — Where Programs Meet Provers
- An axiomatic basis for computer programming
This page was built for publication: Why3-do: the way of harmonious distributed system proofs