/vlsm

Primary LanguageCoqBSD 3-Clause "New" or "Revised" LicenseBSD-3-Clause

VLSM

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.

Meta

Building instructions

The project is compatible with the 2021.09 package pick for Coq 8.13 of Coq Platform release 2021.09.0, so you can obtain all dependencies by installing that Coq Platform variant.

The simplest way of working with this project without needing to install anything is doing so online, by clicking here: Open in Papillon

To instead install dependencies manually via opam, do:

opam repo add coq-released https://coq.inria.fr/opam/released
opam install coq.8.13.2 coq-stdpp.1.5.0

To build the project when you have all dependencies installed, do:

git clone https://github.com/runtimeverification/vlsm.git
cd vlsm
make   # or make -j <number-of-cores-on-your-machine>

Coq file organization

  • theories/VLSM/Lib: Various extensions to the Coq standard library and Coq-std++.
  • theories/VLSM/Core: Core VLSM definitions and theory.

Documentation