package coq-vlsm

  1. Overview
  2. No Docs
Coq formalization of validating labelled state transition and message production systems

Install

Dune Dependency

github.com Edit opam file Versions (4)

Authors

  1. M
    Mihai Calancea
  2. D
    Denisa Diaconescu
  3. W
    Wojciech Kołowski
  4. E
    Elaine Li
  5. B
    Brandon Moore
  6. K
    Karl Palmskog
  7. L
    Lucas Peña
  8. G
    Grigore Roșu
  9. T
    Traian Florin Șerbănuță
  10. I
    Ioan Teodorescu
  11. D
    Dafina Trufaș
  12. J
    Jan Tušil
  13. V
    Vlad Zamfir

Maintainers

  1. P
    palmskog@gmail.com

Sources

v1.3.tar.gz
sha512=9b8810cb5df66db5616fc162090afbe69781490a86e3d828417edd9d32af61a8c4e66591383ad699a245c5fcac795b2ee486737e268152c29f054699fb63a20b

Description

The theory of Validating Labelled State transition and Message production systems (VLSMs) enables describing and proving properties of distributed systems executing in the presence of faults. This project contains a formalization of this theory in the Coq proof assistant along with several examples of distributed protocols modeled and verified using VLSMs, including the ELMO (Equivocation-Limited Message Observer) family of message validating protocols and the Paxos protocol for crash-tolerant distributed consensus.

Tags

category:Computer Science/Concurrent Systems and Protocols/Theory of concurrent systems keyword:consensus keyword:fault tolerance keyword:distributed algorithms keyword:Paxos logpath:VLSM date:2023-12-15

Published: 15 Dec 2023

Dependencies (4)

  1. coq-equations
  2. coq-itauto
  3. coq-stdpp >= "1.9.0"
  4. coq >= "8.16" & < "8.20~"

Dev Dependencies

None

Used by

None

Conflicts

None