coq-verdi.opam

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

homepage: "https://github.com/uwplse/verdi"
dev-repo: "git+https://github.com/uwplse/verdi.git"
bug-reports: "https://github.com/uwplse/verdi/issues"
license: "BSD-2-Clause"

synopsis: "Framework for verification of implementations of distributed systems in Coq"
description: """
Verdi is a Coq framework to implement and formally verify distributed systems.
Verdi supports several different fault models ranging from idealistic to realistic.
Verdi's verified system transformers (VSTs) encapsulate common fault tolerance
techniques. Developers can verify an application in an idealized fault model, and
then apply a VST to obtain an application that is guaranteed to have analogous
properties in a more adversarial environment."""

build: [make "-j%{jobs}%"]
install: [make "install"]
depends: [
  "coq" {>= "8.14"}
  "coq-inf-seq-ext" {= "dev"}
  "coq-struct-tact" {= "dev"}
  "coq-cheerios" {= "dev"}
]

tags: [
  "category:Computer Science/Concurrent Systems and Protocols/Theory of concurrent systems"
  "keyword:program verification"
  "keyword:distributed algorithms"
  "logpath:Verdi"
]
authors: [
  "Justin Adsuara"
  "Steve Anton"
  "Ryan Doenges"
  "Karl Palmskog"
  "Pavel Panchekha"
  "Zachary Tatlock"
  "James R. Wilcox"
  "Doug Woos"
]