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
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
|
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 : 4.5
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.8
, data-default >= 0.7 && < 0.9
, 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.8
, copilot-core >= 4.5 && < 4.6
, copilot-prettyprinter >= 4.5 && < 4.6
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
test-suite unit-tests
type:
exitcode-stdio-1.0
main-is:
Main.hs
other-modules:
Test.Copilot.Theorem.What4
build-depends:
base
, HUnit
, QuickCheck
, test-framework
, test-framework-quickcheck2
, copilot-core
, copilot-theorem
hs-source-dirs:
tests
default-language:
Haskell2010
ghc-options:
-Wall
|
