coq-vlsm.opam

opam-version: "2.0"
maintainer: "palmskog@gmail.com"
version: "dev"

homepage: "https://github.com/runtimeverification/vlsm"
dev-repo: "git+https://github.com/runtimeverification/vlsm.git"
bug-reports: "https://github.com/runtimeverification/vlsm/issues"
license: "BSD-3-Clause"

synopsis: "Coq formalization of validating labelled state transition and message production systems"
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."""

build: ["dune" "build" "-p" name "-j" jobs]
depends: [
  "dune" {>= "3.5"}
  "coq" {>= "8.16"}
  "coq-stdpp" {>= "1.9.0"}
  "coq-itauto"
  "coq-equations"
]

tags: [
  "category:Computer Science/Concurrent Systems and Protocols/Theory of concurrent systems"
  "keyword:consensus"
  "keyword:fault tolerance"
  "keyword:distributed algorithms"
  "keyword:Paxos"
  "logpath:VLSM"
]
authors: [
  "Mihai Calancea"
  "Denisa Diaconescu"
  "Wojciech Kołowski"
  "Elaine Li"
  "Brandon Moore"
  "Karl Palmskog"
  "Lucas Peña"
  "Grigore Roșu"
  "Traian Florin Șerbănuță"
  "Ioan Teodorescu"
  "Dafina Trufaș"
  "Jan Tušil"
  "Vlad Zamfir"
]