@hackage crucible0.9
Crucible is a library for language-agnostic symbolic simulation
Categories
License
BSD-3-Clause
Maintainer
rscott@galois.com, kquick@galois.com, langston@galois.com
Links
Versions
Installation
Dependencies (22)
- async
- base >=4.13 && <4.21
- bimap
- bv-sized >=1.0.0 && <1.1
- containers >=0.5.9.0
- exceptions Show all…
Dependents (7)
@hackage/crucible-syntax, @hackage/copilot-verifier, @hackage/crucible-llvm, @hackage/crux-llvm, @hackage/crucible-symio, @hackage/crux, Show all…
Package Flags
unsafe-operations
(on by default)
Use unsafe operations to improve performance
Crucible provides a program representation format based on single-static assignment (SSA) form control flow graphs, and a symbolic simulation engine for executing programs expressed in this format. It also provides support for communicating with a variety of SAT and SMT solvers, including Z3, CVC4, Yices, STP, and dReal.
For an overview of Crucible please have a look at Lang.Crucible.README