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. J
    Jan Tušil
  11. V
    Vlad Zamfir

Maintainers

  1. P
    palmskog@gmail.com

Sources

v1.1.tar.gz
sha512=9eac41874fea4f622bb7f225b3c6c7f78ca517790ca0b467d571d86476778bdc6e8ea531815cf608b2a9eba966caa21101e90861bce80a10f054ceca53ec65fd

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:fault tolerance keyword:distributed algorithms logpath:VLSM date:2022-02-18

Published: 18 Feb 2022

Dependencies (2)

  1. coq-stdpp >= "1.6.0" & < "1.7.0"
  2. coq >= "8.13" & < "8.15~"

Dev Dependencies

None

Used by

None

Conflicts

None