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 Șerbănuță
  10. D
    Dafina Trufas
  11. J
    Jan Tušil
  12. V
    Vlad Zamfir

Maintainers

  1. P
    palmskog@gmail.com

Sources

v1.2.tar.gz
sha512=5c5ddaef94e17dd7430275717de7958a92af5de15c41b114bad2981157bf17b8c8e01e33686339fcb80bdbbae660d86dce592954a4be884a3be8d423b692f262

Description

A validating labelled state transition and message production system (VLSM) abstractly models a distributed system with faults. This project contains a formalization of VLSMs and their theory in the Coq proof assistant.

Tags

category:Computer Science/Concurrent Systems and Protocols/Theory of concurrent systems keyword:consensus keyword:fault tolerance keyword:distributed algorithms logpath:VLSM date:2022-10-11

Published: 13 Oct 2022

Dependencies (4)

  1. coq-equations
  2. coq-itauto
  3. coq-stdpp >= "1.7.0" & < "1.8.0"
  4. coq >= "8.15" & < "8.18~"

Dev Dependencies

None

Used by

None

Conflicts

None