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.3
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.7
, copilot-core >= 4.3 && < 4.4
, copilot-prettyprinter >= 4.3 && < 4.4
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