kind2.opam

# This file is generated by dune, edit dune-project instead
opam-version: "2.0"
synopsis:
  "Multi-engine, parallel, SMT-based automatic model checker for safety properties of Lustre programs"
description: """
Kind 2 is a multi-engine, parallel, SMT-based automatic model checker for safety properties of Lustre programs.

Kind 2 takes as input a Lustre file annotated with properties to be proven invariant, and outputs which of the properties are true for all inputs, as well as an input sequence for those properties that are falsified. To ease processing by external tools, Kind 2 can output its results in JSON and XML formats.

By default Kind 2 runs a process for bounded model checking (BMC), a process for k-induction, two processes for invariant generation, and a process for IC3 in parallel on all properties simultaneously. It incrementally outputs counterexamples to properties as well as properties proved invariant."""
maintainer: ["Kind2 developers"]
authors: ["Kind2 developers"]
license: "Apache-2.0"
homepage: "https://kind2-mc.github.io/kind2"
doc: "https://kind.cs.uiowa.edu/kind2_user_doc"
bug-reports: "https://github.com/kind2-mc/kind2/issues"
depends: [
  "ocaml" {>= "4.07"}
  "dune"
  "dune-build-info"
  "menhir"
  "num"
  "yojson"
  "zmq"
]
build: [
  ["dune" "subst"] {pinned}
  [
    "dune"
    "build"
    "-p"
    name
    "-j"
    jobs
    "@install"
    "@runtest" {with-test}
    "@doc" {with-doc}
  ]
]
dev-repo: "git+https://github.com/kind2-mc/kind2.git"