See PDF. This is a very rough draft. Use it on your own risk.
The main goal of the document is to propose a formal model of
- concrete execution,
- symbolic execution,
- dynamic symbolic (concolic) execution,
- and taint tracking.
Run python run.py to create PDF file main.pdf.
Requirements:
- LaTeX,
- Python 3 (for SVG graph generation),
- Inkscape (for image conversion from SVG to PDF).
There is also a simple graph drawing Python module. It is used to generate execution sequences, execution paths, control flow graphs, and symbolic execution trees.