Author: David Pichardie
Title: A Modular Lattice Library to Develop Certified Terminating Static Analyses
Abstract: 
We present a framework to develop and extract certified
static analysis in the Coq proof assistant. Using the abstract
interpretation methodology, static analyses are specified as least
solution of system of equations (inequations) on lattice structures. A
library of Coq modules is proposed to construct complex and efficient
lattices by combination of functors. The lattice signature possesses a
parameter which ensure termination of a generic fixed-point
solver. The delicate problem of termination is hence solved by
combination of the different lattice functors. This talk will focus on
the extension of this termination property into a more general one
which allow to certify more sophisticated static analyses. We will
present the different proposed functors and sketch their different
(constructive) proofs.