Awesome

Awesome Symbolic Execution

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

Table of Contents

• Papers
• Courses
• Videos
• Tools

Papers

• Symbolic Execution and Program Testing, James C. King.
• A system to generate test data and symbolically execute programs, L. A. Clarke.
• All You Ever Wanted to Know about Dynamic Taint Analysis and Forward Symbolic Execution (but Might Have Been Afraid to Ask), Edward J. Schwartz, Thanassis Avgerinos, David Brumley.
• Symbolic Execution for Software Testing: Three Decades Later, Cristian Cadar and Koushik Sen
• A Survey of Symbolic Execution Techniques, Roberto Baldoni, Emilio Coppa, Daniele Cono D’Elia, Camil Demetrescu, and Irene Finocchi.
• Collection of symbolic execution papers: XMUsuny/symbolic-execution-papers

Courses

• Symbolic Execution Lecture at Harvard.
• Symbolic Execution Lecture at Iowa State University.
• Symbolic Execution Lecture at University of Maryland.

Videos

• Symbolic Execution Lecture at MIT.
• Symbolic Execution Lecture (part of Software Security course on Coursera).
• Program Analysis course by Prof. Dr. Michael Pradel at University of Stuttgart
  • Symbolic and Concolic Testing (Part 1, Symbolic)
  • Symbolic and Concolic Testing (Part 2, Challenges)
  • Symbolic and Concolic Testing (Part 3, Concolic)
  • Symbolic and Concolic Testing (Part 4, Applications)

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).
• SWAT - Loosely coupled dynamic symbolic execution using ASM for instrumentation, JavaSMT for formula generation and currently Z3 as a solver.

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.
• GenSym - A compiler for parallel fork-based symbolic execution.

.NET

• PEX - Dynamic symbolic execution tool for .NET.

C

• CREST - is an open-source tool for concolic testing of C programs.
• Otter - is a pure, source-level symbolic executor for C that can be used to test programs.
• CIVL - A framework that includes the CIVL-C programming language, a model checker and a symbolic execution tool.

JavaScript

• Jalangi2 - Dynamic analysis framework for JavaScript.
• SymJS - Automatic symbolic testing of JavaScript web applications.

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

• SymDroid - A Symbolic Executor to Identify Activity Permission in Android Application.

Binaries

• Mayhem.
• SAGE - Whitebox file fuzzing tool for X86 Windows applications.
• DART - is the first concolic testing tool that combines dynamic test generation.
• BitBlaze - Binary Analysis for Computer Security.
• 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.
• Sydr-Fuzz - Continuous Hybrid Fuzzing and Dynamic Analysis for Security Development Lifecycle.
• SymEx-VP - Symbolic execution for RISC-V embedded firmware with accurate SystemC peripheral models.

Misc

• Symbooglix - Symbolic execution tool for Boogie programs.
• OSS-Sydr-Fuzz - Hybrid Fuzzing for Open Source Software