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…

, 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.

Symbolic Execution Lecture at Harvard

.

Symbolic Execution Lecture at Iowa State University

.

Symbolic Execution Lecture at University of Maryland

.

Symbolic Execution Lecture at MIT

.

Symbolic Execution Lecture (part of Software Security course on Coursera)

.

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)

Owi

Parallel (dynamic) symbolic execution engine built on WebAssembly (Wasm) that can run Rust code.

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.

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.

Owi

Parallel (dynamic) symbolic execution engine built on WebAssembly (Wasm) that can run Rust code.

PEX

Dynamic symbolic execution tool for .NET.

VSharp

Symbolic execution engine for .NET assemblies.

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.

Owi

Parallel (dynamic) symbolic execution engine built on WebAssembly (Wasm) that can run Rust code.

Jalangi2

Dynamic analysis framework for JavaScript.

SymJS

Automatic symbolic testing of JavaScript web applications.

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.

APEX

Concolic execution engine for Python with coverage-guided test generation. Built in Rust.

Rubyx

Symbolic execution tool for Ruby on Rails web apps.

SymDroid

A Symbolic Executor to Identify Activity Permission in Android Application.

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.

Owi

Parallel (dynamic) symbolic execution engine built on WebAssembly (Wasm) that can run Rust code.

Symbooglix

Symbolic execution tool for Boogie programs.

OSS-Sydr-Fuzz

Hybrid Fuzzing for Open Source Software