Why3-do: the way of harmonious distributed system proofs

DOI10.1007/978-3-030-99336-8_5MaRDI QIDQ6166787zbMATH OpenOpenAlexFDO

Authors Cláudio Belo Lourenço, Jorge Sousa Pinto

Publication date 3 August 2023

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

Copyright license Creative Commons Attribution 4.0 International

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

Mathematics Subject Classification ID

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

Recommendations

• Why3 -- where programs meet provers
• Aneris: a mechanised logic for modular reasoning about distributed systems
• Verifying distributed systems: the operational approach
• Formal Verification of Distributed Algorithms
• Towards Automated Proof Support for Probabilistic Distributed Systems

Cites work

• An axiomatic basis for computer programming
• An improved algorithm for decentralized extrema-finding in circular configurations of processes
• Aneris: a mechanised logic for modular reasoning about distributed systems
• Dafny: an automatic program verifier for functional correctness
• scientific article; zbMATH DE number 1809861 (Why is no real title available?)
• scientific article; zbMATH DE number 194642 (Why is no real title available?)
• scientific article; zbMATH DE number 5585443 (Why is no real title available?)
• Model checking
• One logic to use them all
• Self-stabilizing systems in spite of distributed control
• Software engineering and formal methods. 10th international conference, SEFM 2012, Thessaloniki, Greece, October 1--5, 2012. Proceedings
• The existence of refinement mappings
• Why3 -- where programs meet provers

This page was built for publication: Why3-do: the way of harmonious distributed system proofs

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6166787)