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
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
|
cabal-version : >= 1.10
name : copilot-theorem
synopsis: k-induction for Copilot.
description:
Some tools to prove properties on Copilot programs with k-induction model
checking.
.
Copilot is a stream (i.e., infinite lists) domain-specific language (DSL) in
Haskell that compiles into embedded C. Copilot contains an interpreter,
multiple back-end compilers, and other verification tools.
.
A tutorial, examples, and other information are available at
<https://copilot-language.github.io>.
version : 3.13
license : BSD3
license-file : LICENSE
maintainer : Ivan Perez <ivan.perezdominguez@nasa.gov>
homepage : https://copilot-language.github.io
bug-reports : https://github.com/Copilot-Language/copilot/issues
stability : Experimental
category : Language, Embedded
build-type : Simple
extra-source-files : README.md
, CHANGELOG
author : Jonathan Laurent
x-curation: uncurated
source-repository head
type: git
location: https://github.com/Copilot-Language/copilot.git
subdir: copilot-theorem
library
default-language : Haskell2010
hs-source-dirs : src
ghc-options : -Wall
-fno-warn-name-shadowing
-fno-warn-unused-binds
-fno-warn-missing-signatures
-fcontext-stack=100
build-depends : base >= 4.9 && < 5
, bimap (>= 0.3 && < 0.4) || (>= 0.5 && < 0.6)
, bv-sized >= 1.0.2 && < 1.1
, containers >= 0.4 && < 0.7
, data-default >= 0.7 && < 0.8
, directory >= 1.3 && < 1.4
, libBF >= 0.6.2 && < 0.7
, mtl >= 2.0 && < 2.4
, panic >= 0.4.0 && < 0.5
, parsec >= 2.0 && < 3.2
, parameterized-utils >= 2.1.1 && < 2.2
, pretty >= 1.0 && < 1.2
, process >= 1.6 && < 1.7
, random >= 1.1 && < 1.3
, transformers >= 0.5 && < 0.7
, xml >= 1.3 && < 1.4
, what4 >= 1.3 && < 1.4
, copilot-core >= 3.13 && < 3.14
, copilot-prettyprinter >= 3.13 && < 3.14
exposed-modules : Copilot.Theorem
, Copilot.Theorem.Prove
, Copilot.Theorem.Kind2
, Copilot.Theorem.Prover.SMT
-- , Copilot.Theorem.Prover.Z3
, Copilot.Theorem.Kind2.Prover
, Copilot.Theorem.What4
other-modules : Copilot.Theorem.Tactics
, Copilot.Theorem.IL
, Copilot.Theorem.IL.PrettyPrint
, Copilot.Theorem.IL.Spec
, Copilot.Theorem.IL.Translate
, Copilot.Theorem.IL.Transform
, Copilot.Theorem.Kind2.AST
, Copilot.Theorem.Kind2.Output
, Copilot.Theorem.Kind2.PrettyPrint
, Copilot.Theorem.Kind2.Translate
, Copilot.Theorem.Prover.SMTIO
, Copilot.Theorem.Prover.SMTLib
, Copilot.Theorem.Prover.TPTP
, Copilot.Theorem.Prover.Backend
, Copilot.Theorem.Misc.Error
, Copilot.Theorem.Misc.SExpr
, Copilot.Theorem.Misc.Utils
, Copilot.Theorem.TransSys
, Copilot.Theorem.TransSys.Cast
, Copilot.Theorem.TransSys.PrettyPrint
, Copilot.Theorem.TransSys.Renaming
, Copilot.Theorem.TransSys.Spec
, Copilot.Theorem.TransSys.Transform
, Copilot.Theorem.TransSys.Translate
, Copilot.Theorem.TransSys.Invariants
, Copilot.Theorem.TransSys.Operators
, Copilot.Theorem.TransSys.Type
, Copilot.Theorem.What4.Translate
|
