Détails sur le séminaire

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

Contact | Plan du site | Site réalisé avec SPIP 3.2.16 + AHUNTSIC [CC License]

info visites 1876602