Certified Impossibility Results and Analyses in Coq of Some Randomised Distributed Algorithms

DOI10.1007/978-3-319-46750-4_5zbMath1482.68282OpenAlexW2523222593MaRDI QIDQ3179391

Akka Zemmari, Allyx Fontaine

Publication date: 21 December 2016

Published in: Theoretical Aspects of Computing – ICTAC 2016 (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-319-46750-4_5

Mathematics Subject Classification ID

Analysis of algorithms (68W40) Randomized algorithms (68W20) Distributed algorithms (68W15) Formalization of mathematics in connection with theorem provers (68V20) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items (1)

Certified Impossibility Results and Analyses in Coq of Some Randomised Distributed Algorithms

Uses Software

• Coq
• PRISM
• RDA

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Impossibility of gathering, a certification
• Proofs of randomized algorithms in Coq
• Analysis of a randomized rendezvous algorithm
• Finite state Markovian decision processes
• Formal Verification of Distributed Algorithms
• Certified Impossibility Results and Analyses in Coq of Some Randomised Distributed Algorithms
• Formal verification of timed properties of randomized distributed algorithms

This page was built for publication: Certified Impossibility Results and Analyses in Coq of Some Randomised Distributed Algorithms