Vincent Laporte

Vērification d’analyses statiques pour langages de bas niveau

This page references the Coq developments related to my Ph.D., “Verification of static analyzes for low-level languages”.

Preliminary version of the manuscript

Abstract-Interpretation-Based Static Analysis with Coq

Coq source

CFG analyzer

Depends on CompCert 1.11 ported to Coq 8.4 with the additional CFG intermediate language.

Source code of the CFG analyzer

Self-modifying programs

Control-flow graph of a flattened, self-modifying, computation of the Fibonacci sequence

Source code of the GOTO★ analyzer

Sample analyzed programs:

Memory domain

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 vanalysis directory.

Verasco C♯minor analyzer

Please refer to the Verasco analyzer homepage.