@hackage / copilot-verifier

System for verifying the correctness of generated Copilot programs

Latest4.8

Dependencies

library:copilot-verifier (23 dependencies)

@hackage / lens Lenses, Folds and Traversals
- Version:
- License: BSD-2-Clause
@hackage / crux Simple top-level library for Crucible Simulation
- Version: >=0.7.1 && <0.8
- License: BSD-3-Clause
@hackage / prettyprinter A modern, easy to use, well-documented, extensible pretty-printer.
- Version: >=1.7.0
- License: BSD-2-Clause
@hackage / base Core data structures and operations
- Version: >=4.8 && <4.20
- License: BSD-3-Clause
@hackage / copilot-core An intermediate representation for Copilot.
- Version: >=4.8 && <4.9
- License: BSD-3-Clause
@hackage / filepath Library for manipulating FilePaths in a cross platform way.
- Version:
- License: BSD-3-Clause
@hackage / parameterized-utils Classes and data structures for working with data-kind indexed types
- Version: >=2.1.4 && <2.2
- License: BSD-3-Clause
@hackage / crux-llvm A verification tool for C programs.
- Version: >=0.9 && <0.10
- License: BSD-3-Clause
@hackage / copilot-c99 A compiler for Copilot targeting C99.
- Version: >=4.8 && <4.9
- License: BSD-3-Clause
@hackage / mtl Monad classes for transformers, using functional dependencies
- Version:
- License: BSD-3-Clause
@hackage / what4 Solver-agnostic symbolic values support for issuing queries
- Version: >=1.6.1 && <1.8
- License: BSD-3-Clause
@hackage / copilot-theorem k-induction for Copilot.
- Version: >=4.8 && <4.9
- License: BSD-3-Clause
@hackage / crucible-llvm Support for translating and executing LLVM code in Crucible
- Version: >=0.7 && <0.8
- License: BSD-3-Clause
@hackage / text An efficient packed Unicode text type.
- Version:
- License: BSD-2-Clause
@hackage / transformers Concrete functor and monad transformers
- Version:
- License: BSD-3-Clause
@hackage / aeson Fast JSON parsing and encoding
- Version: >=1.5 && <2.3
- License: BSD-3-Clause
@hackage / bv-sized a bitvector datatype that is parameterized by the vector width
- Version: >=1.0.0 && <1.1
- License: BSD-3-Clause
@hackage / vector Efficient Arrays
- Version:
- License: BSD-3-Clause
@hackage / containers Assorted concrete container types
- Version: >=0.5.9.0
- License: BSD-3-Clause
@hackage / panic A convenient way to panic.
- Version: >=0.3
- License: ISC
@hackage / bytestring Fast, compact, strict and lazy byte strings with a list interface
- Version:
- License: BSD-3-Clause
@hackage / llvm-pretty A pretty printing library inspired by the llvm binding.
- Version: >=0.12.1.0 && <0.13
- License: BSD-3-Clause
@hackage / crucible Crucible is a library for language-agnostic symbolic simulation
- Version: >=0.7.1 && <0.8
- License: BSD-3-Clause

library:copilot-verifier-examples (29 dependencies)

executable:verify-examples (26 dependencies)

test:copilot-verifier-test (29 dependencies)