- 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.svg for the latest version.
SAT and SMT solving
solving.svg for the latest version.
Building PNG or PDF
Please, install fonts for correct SVG display:
Use Inkscape to build PNG or PDF. Example for
inkscape diagram/symbolic-execution.svg --export-png diagram/symbolic-execution.png --export-dpi 150,
inkscape diagram/symbolic-execution.svg --export-pdf diagram/symbolic-execution.pdf.
We use colors from GitHub Linguist for input languages.
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).
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.yml contains tools YAML description. E.g.:
DART: since: 2005 input: C uses: lp_solve based: CIL description: random testing and direct execution