Séminaire d'équipe(s) Verification of Algorithms, Languages and Systems
Coq, the world's best macro assembler!
Pierre-Évariste Dagand
07 February 2014, 10:00 - 07 February 2014, 11:30 Salle/Bat : 445/PCRI-N
Contact :
Activités de recherche : Formalisation of (Specification and Programming) Languages in Proof Assistants
Résumé :
With Nick Benton and Andrew Kennedy (Microsoft Research Cambridge), I
have worked on CoqOS, a Coq library for programming and verifying x86
assembly programs. This library offers an operational semantics of (a
significant subset of) the x86 CPU, a certified assembler, and a
separation logic for reasoning about x86 assembly programs. In this
framework, I have implemented a regular expression compiler and proved
its correctness : the resulting x86 code accepts a word iff the regexp
matches that word.
I will first give a brief introduction to CoqOS, demonstrating a few
of its salient features. I shall put a special emphasis on its program
logic, which is obtained by elegant algebraic means. I will then
illustrate its workings with some of the programming and proving
patterns used in my certified compiler.
