A curated list of awesome symbolic execution resources including essential research papers, lectures, videos, and tools.
Fundamental papers:
- SELECT—a formal system for testing and debugging programs by symbolic execution, R. S. Boyer, B. Elspas, K. N. Levitt. 1975.
- Symbolic Execution and Program Testing, James C. King. 1976.
- A System to Generate Test Data and Symbolically Execute Programs, L. A. Clarke. 1976.
Symbolic execution survey:
- 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. 2010.
- A Survey of Symbolic Execution Techniques, Roberto Baldoni, Emilio Coppa, Daniele Cono D’Elia, Camil Demetrescu, and Irene Finocchi. 2016—2017.
- 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 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).
- KLEE - Symbolic execution engine built on LLVM. Uses STP.
- Cloud9 - Parallel symbolic execution engine built on KLEE.
- Kite - Based on KLEE and LLVM.
- CREST.
- DART - A tool that performs directed automated random testing of C programs. Uses CIL and lp_solve.
- Otter - A directed symbolic execution tool that is used to reach a particular target line. Uses STP.
- CIVL - A framework that includes the CIVL-C programming language, a model checker and a symbolic execution tool.
- CUTE - A concolic unit testing engine for C. Uses CIL and lp_solve.
- Jalangi2 - A framework for writing dynamic analyses for JavaScript.
- SymJS - Automatic symbolic testing of JavaScript web applications. Uses Yices.
- PyExZ3 - Symbolic execution of Python functions. A rewrite of the NICE project's symbolic execution tool.
- Mayhem - A system for finding exploitable bugs in binary programs. Is based on hybrid (online and offline) dynamic symbolic execution. Uses Pin and BAP as well as Z3. The winner of 2016 DARPA CGC.
- SAGE - Whitebox file fuzzing tool for X86 Windows applications. Uses Z3.
- BitBlaze - A binary analysis platform. Uses STP.
- 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. Based on QEMU, KLEE, and LLVM.
- 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. Based on VEX, Unicorn, and Z3.
- Triton - Dynamic binary analysis platform that includes a dynamic symbolic execution tool based on Pin and Capstone.
- manticore - symbolic execution tool for binaries (x86, x86_64 and ARMV7) and Ethereum smart contract bytecode
- Symbooglix - Symbolic execution tool for Boogie programs.