salle A. Turing CE4
23 janvier 2014 - 15h00
Verifying numerical static analysis results with a proof assistant
par Alexis Fouilhe de Verimag
Abstract: This talk will give an overview of my PhD work, both accomplished an
projected. The main focus is on adapting existing numerical static
analysis techniques so that their result can be proved correct using
the Coq proof assistant.
To start with, a lightweight approach to proving the correctness of an
implementation of the abstract domain of polyhedra will be described.
I will then move to ongoing and projected work. Handling the specifics
of machine arithmetic, which is required to be able to prove correctness
of analysis results, will come first. Then, I will present plans to
extend the two-phase architecture used for polyhedra to a complete static
analyzer.
