bap-primus-symbolic-executor

Primus Symbolic Executor
Description

Provides the bap:symbolic-executor Primus system that uses an SMT solver (z3) to compute inputs for as many paths as possible. It also includes the symbolic-computer component that computes symbolic formulas for each value that depends on input and provides Primus Lisp primitives to create symbolic values and symbolic memories, as well as to specify additional constraints and post asserts that are dispatched to the SMT solver.

Install
Documentation failed to build! Sorry about that.
Published
14 Jul 2022
Authors
Sources
v2.5.0.tar.gz
md5=5abd9b3628b43f797326034f31ca574f
Dependencies
z3
>= "4.8.8-1" & < "4.8.13"
regular
= "2.5.0"
monads
= "2.5.0"
bitvec
= "2.5.0"
bap-primus
= "2.5.0"
bap-std
= "2.5.0"
bap-main
= "2.5.0"
core_kernel
>= "v0.14" & < "v0.16"
ocaml
>= "4.08.0"
Reverse Dependencies
bap-extra
>= "2.5.0"