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.0.tar.gz
sha512=9bfcc12a4aeba66d23daa8783c28d575d135dbeb4956229df187a58f005594106f45920ee474fff4375a9e59fb11c9cf42958808b45ede97d80c67f0027b162b

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:2021-12-23

Published: 09 Feb 2022

Dependencies (2)

  1. coq-stdpp = "1.5.0"
  2. coq >= "8.13" & < "8.14~"

Dev Dependencies

None

Used by

None

Conflicts

None