Awesome
Timeline diagrams
This repository contains manually drawn diagrams with timelines, as well as Kotlin code for generating similar types of diagrams. However, please note that the code is not fully functional yet and currently produces diagrams that are graphically less refined compared to the manually created ones.
Manually drawn diagrams
Symbolic execution
See the latest version in
symbolic-execution.svg
.
The symbolic execution timeline highlights key tools and concepts in pure symbolic execution, dynamic symbolic execution (concolic testing), as well as related ideas of model checking, SAT/SMT solving, black-box fuzzing, taint data tracking, and other dynamic analysis techniques.
SAT and SMT solving
See the latest version in solving.svg
.
The solving timeline showcases major SAT and SMT techniques and solvers, including those not directly related to symbolic execution.
Additionally, there is a temporary timeline for some tools that are not displayed in the diagrams above.
Building PNG and PDF
Please install the following fonts for correct SVG display:
Use Inkscape to build PNG or PDF files. Example for the 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 to SVG files
Feel free to suggest changes or add new information. If your change is minor
(like fixing a typo), you can directly edit the source code of
symbolic-execution.svg
. For major changes,
you're encouraged to either create a new issue or edit symbolic-execution.svg
.
The Inkscape editor is strongly recommended due to
source code compatibility issues.
Before commiting
Please use SVGO for diagram optimization before commiting (to achieve a cleaner diff):
svgo diagram/symbolic-execution.svg \
--pretty \
--enable=sortAttrs \
--disable=removeEditorsNSData \
--disable=cleanupIDs \
--indent=2
Automatic diagram generation
The repository also includes Kotlin code that automatically generates similar
diagrams using the tools.json
file, which contains
descriptions of the tools, and a config
file that guides the
generator on how to arrange and draw the elements.
Tools structure
File tools.json
contains tools JSON description. E.g.:
{
"name": "DART",
"since": 2005,
"languages": ["C"],
"uses": ["lp_solve"],
"based": ["CIL"],
"description": "random testing\nand direct\nexecution",
"type": "concolic",
"authors": ["P. Godefroid (B)", "K. Sen (I)", "N. Klarlund (B)"]
},