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 . version : 3.12 license : BSD3 license-file : LICENSE maintainer : Ivan Perez 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.12 && < 3.13 , copilot-prettyprinter >= 3.12 && < 3.13 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