This page references the Coq developments related to my Ph.D., “Verification of static analyzes for low-level languages”.
Preliminary version of the manuscript
Depends on CompCert 1.11 ported to Coq 8.4 with the additional CFG intermediate language.
Source code of the CFG analyzer
Source code of the GOTO★ analyzer
Sample analyzed programs:
The source code relevant to this chapter is part of the CFG analyzer above. The relevant files are
PointsTo.v (type and points-to domain),
Nconvert.v (numerical conversion),
FMem.v (intermediate specification of the concrete memory), and
MemCFG.v (abstract memory domain) in the
Please refer to the Verasco analyzer homepage.