Skip to content
A curated list of awesome symbolic execution resources including essential research papers, lectures, videos, and tools.
Branch: master
Clone or download
Permalink
Type Name Latest commit message Commit time
Failed to load latest commit information.
LICENSE Init commit Jul 18, 2017
README.md Updated S2E website Aug 13, 2018
contributing.md Add contribution guidelines (modified version of Jul 18, 2017

README.md

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

  • 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

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

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.
You can’t perform that action at this time.