工具与框架
最后更新于
Java
- Symbolic execution tool built on . Supports multiple constraint solvers, lazy initialization, etc.
- Dynamic symbolic execution tool built on . Supports multiple constraint solvers using .
- Concolic execution tool that uses for instrumentation. Uses CVC4.
- Concolic execution tool that uses for instrumentation. Supports and . Concolic execution can be distributed.
- Concolic execution tool that uses for instrumentation. Originally for Android analysis. Supports .
- Concolic execution tool that uses for instrumentation. Supports .
- Concolic execution tool built on .
- Symbolic execution tool that uses a custom JVM. Supports CVC3, CVC4, Sicstus, and Z3.
- Theorem Prover that uses specifications written in Java Modeling Language (JML).
LLVM
- Symbolic execution engine built on LLVM.
- Parallel symbolic execution engine built on KLEE.
- Based on KLEE and LLVM.
.NET
- Dynamic symbolic execution tool for .NET.
C
JavaScript
Python
Ruby
Android
Binaries
Misc
.
.
- A framework that includes the CIVL-C programming language, a model checker and a symbolic execution tool.
.
.
- Symbolic execution of Python functions. A rewrite of the project's symbolic execution tool.
- Symbolic execution tool for Ruby on Rails web apps.
.
.
- Whitebox file fuzzing tool for X86 Windows applications.
.
.
- Path-based dynamic analysis for 32-bit programs.
- Symbolic execution tool built on the BitBlaze Vine component.
- Symbolic execution platform supporting x86, x86-64, or ARM software stacks.
- Reverse engineering framework. Includes symbolic execution.
- Supports x86/x64 binaries.
- Binary Analysis Platform provides a framework for writing program analysis tools.
- Python framework for analyzing binaries. Includes a symbolic execution tool.
- Dynamic binary analysis platform that includes a dynamic symbolic execution tool.
- Symbolic execution tool for binaries (x86, x86_64 and ARMV7) and Ethereum smart contract bytecode.
- Symbolic execution tool for Boogie programs.