kind2/dune-project at develop · lorchrob/kind2 · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
(lang dune 2.7)

(name kind2)

(license Apache-2.0)
(authors "The Kind 2 development team")
(maintainers "Daniel Larraz <daniel-larraz@uiowa.edu>")
(source
  (github kind2-mc/kind2))

(package
 (name kind2)
 (synopsis
   "Multi-engine, parallel, SMT-based automatic model checker for safety properties of Lustre programs")
 (description "Kind 2 is an open-source, multi-engine, SMT-based automatic model checker for safety properties of finite-state
or infinite-state synchronous reactive systems expressed as in an extension of the Lustre language.
In its basic configuration it takes as input a Lustre file annotated with properties to be proven invariant,
and outputs for each property either a confirmation or a counterexample, i.e., a sequence inputs that falsifies the property.
More advanced features include contract-based compositional verification, proof generation for proven properties, and contract-based test generation.")
 (homepage "https://kind2-mc.github.io/kind2")
 (documentation "https://kind.cs.uiowa.edu/kind2_user_doc")
 (depends
  (ocaml
   (>= 4.14))
  dune
  dune-build-info
  (menhir
   (>= 20180523)) ; Required by dune when the infer option is used
                  ; See issue: https://github.com/ocaml/dune/issues/1392
  num
  (odoc :with-doc)
  (ounit2 :with-test)
  yojson
  (zmq
   (>= 5.1.0))
 )
)

(package
 (name kmoxi)
 (synopsis "A model checker for the MoXI language based on Kind 2")
 (description "kMoXI is a model checker for the MoXI language that uses Kind 2 back-end technology for model checking")
 (homepage "https://kind2-mc.github.io/kind2")
 (depends
  (ocaml
   (>= 4.14))
  dune
  dune-build-info
  (menhir
   (>= 20180523)) ; Required by dune when the infer option is used
                  ; See issue: https://github.com/ocaml/dune/issues/1392
  num
  (odoc :with-doc)
  (ounit2 :with-test)
  yojson
  (zmq
   (>= 5.1.0))
 )
)

(using menhir 2.0)

(generate_opam_files true)