History of symbolic execution (as well as SAT/SMT solving, fuzzing, and taint data tracking)
There is also temporary timeline of some tools not displayed in the diagrams above.
:warning: PNG preview could be outdated. See symbolic-execution.svg
for the latest version.
:warning: PNG preview could be outdated. See solving.svg
for the latest version.
Please, install fonts for correct SVG display:
Use Inkscape to build PNG or PDF. Example for symbolic-execution
diagram:
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
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