工具与框架

Java

• JPF-Symbc - Symbolic execution tool built on Java PathFinder. Supports multiple constraint solvers, lazy initialization, etc.

• JDart - Dynamic symbolic execution tool built on Java PathFinder. Supports multiple constraint solvers using JConstraints.

• CATG - Concolic execution tool that uses ASM for instrumentation. Uses CVC4.

• LimeTB - Concolic execution tool that uses Soot for instrumentation. Supports Yices and Boolector. Concolic execution can be distributed.

• Acteve - Concolic execution tool that uses Soot for instrumentation. Originally for Android analysis. Supports Z3.

• jCUTE - Concolic execution tool that uses Soot for instrumentation. Supports lp_solve.

• JFuzz - Concolic execution tool built on Java PathFinder.

• JBSE - Symbolic execution tool that uses a custom JVM. Supports CVC3, CVC4, Sicstus, and Z3.

• Key - Theorem Prover that uses specifications written in Java Modeling Language (JML).

LLVM

• KLEE - Symbolic execution engine built on LLVM.

• Cloud9 - Parallel symbolic execution engine built on KLEE.

• Kite - Based on KLEE and LLVM.

.NET

• PEX - Dynamic symbolic execution tool for .NET.

C

• CREST.

• Otter.

• CIVL - A framework that includes the CIVL-C programming language, a model checker and a symbolic execution tool.

JavaScript

• Jalangi2.

• SymJS.

Python

• PyExZ3 - Symbolic execution of Python functions. A rewrite of the NICE project's symbolic execution tool.

Ruby

• Rubyx - Symbolic execution tool for Ruby on Rails web apps.

Android

• SymDroid.

Binaries

• Mayhem.

• SAGE - Whitebox file fuzzing tool for X86 Windows applications.

• DART.

• BitBlaze.

• PathGrind - Path-based dynamic analysis for 32-bit programs.

• FuzzBALL - Symbolic execution tool built on the BitBlaze Vine component.

• S2E - Symbolic execution platform supporting x86, x86-64, or ARM software stacks.

• miasm - Reverse engineering framework. Includes symbolic execution.

• pysymemu - Supports x86/x64 binaries.

• BAP - Binary Analysis Platform provides a framework for writing program analysis tools.

• angr - Python framework for analyzing binaries. Includes a symbolic execution tool.

• Triton - Dynamic binary analysis platform that includes a dynamic symbolic execution tool.

• manticore - Symbolic execution tool for binaries (x86, x86_64 and ARMV7) and Ethereum smart contract bytecode.

Misc

• Symbooglix - Symbolic execution tool for Boogie programs.