/symbolic-execution

History of symbolic execution (as well as SAT/SMT solving, fuzzing, and taint data tracking)

Primary LanguageKotlinCreative Commons Attribution Share Alike 4.0 InternationalCC-BY-SA-4.0

Timelines

  • Symbolic execution timeline highlights some major tools and ideas of pure symbolic execution, dynamic symbolic execution (concolic) as well as related ideas of model checking, SAT/SMT solving, black-box fuzzing, taint data tracking, and other dynamic analysis techniques.
  • Solving timeline highlights major SAT and SMT techniques and solvers (including solvers not related to symbolic execution).

There is also temporary timeline of some tools not displayed in the diagrams above.

Symbolic execution

⚠️ PNG preview could be outdated. See symbolic-execution.svg for the latest version.

Preview

SAT and SMT solving

⚠️ PNG preview could be outdated. See solving.svg for the latest version.

Preview

Building PNG or PDF

Please, install fonts for correct SVG display:

Use Inkscape to build PNG or PDF. Example for symbolic-execution diagram:

  • PNG: inkscape diagram/symbolic-execution.svg --export-png diagram/symbolic-execution.png --export-dpi 150,
  • PDF: inkscape diagram/symbolic-execution.svg --export-pdf diagram/symbolic-execution.pdf.

Design

We use colors from GitHub Linguist for input languages.

Contribution

Feel free to suggest changes or add new information. If your change is minor (like typo), you can just edit source code of symbolic-execution.svg. If change is major, you are encouraged to either create new issue, or edit symbolic-execution.svg (Inkscape editor is strongly recommended due to source code issues).

Before commiting

Please, use SVGO for diagram optimization before commiting (to get more clean diff):

svgo diagram/symbolic-execution.svg \
    --pretty \
    --enable=sortAttrs \
    --disable=removeEditorsNSData \
    --disable=cleanupIDs \
    --indent=2

Tools structure

File tools.yml contains tools YAML description. E.g.:

DART:
  since: 2005
  input: C
  uses: lp_solve
  based: CIL
  description: random testing and direct execution

Tool explanation

How the tool is articulated ?

We have 2 config files to see if we need to change anything on the information within the image. One file is the folder tool and is named tools.json. This Json has all the tool references. One Tool is represented as the following : { "name": , "since": , "description": , "url": , "github": , "type": , "uses":[""], "affilications":["",""], "os": , "license": , "languages": ["",""], "api": , "technique": , "authors": , }

The other file is config and this is describing the links between the tools in tools.json.

This help keeping track on the timeline interaction between tools.