/research-symbolic-execution

A curated list of awesome symbolic execution resources including essential research papers, lectures, videos, and tools.

Creative Commons Zero v1.0 UniversalCC0-1.0

Awesome Symbolic Execution Awesome

A curated list of awesome symbolic execution resources including essential research papers, lectures, videos, and tools.

Table of Contents

Papers

Courses

Videos

Tools

Java

  • Symbolic PathFinder (SPF) - 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.
  • SymCC - A compiler wrapper which embeds symbolic execution into the program during compilation, and an associated run-time support library.

.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

Python

  • CrossHair - Symbolic execution tool for verifying properties of Python functions.
  • 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

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.
  • MAAT - Low-level symbolic execution tool, uses Ghidra's p-code.
  • BinCAT - Binary code static analyser, with IDA integration. Performs value and taint analysis, type reconstruction, use-after-free and double-free detection.

Misc

  • Symbooglix - Symbolic execution tool for Boogie programs.