Skip to content

Formal model of program execution, symbolic execution, and taint tracking

Notifications You must be signed in to change notification settings

enzet/program-model

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 

History

91 Commits
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 

Repository files navigation

Program execution formal model

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.

Build (Linux and macOS)

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).

Graph drawing

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.

Releases

No releases published

Packages

No packages published