Français Anglais
Accueil Annuaire Plan du site
Accueil > Evenements > Séminaires
Séminaire d'équipe(s) VALS
Coq, the world's best macro assembler!
Pierre-Évariste Dagand

07 February 2014, 10h00 - 07 February 2014, 11h30
Salle/Bat : 445/PCRI-N
Contact :

Activités de recherche : Formalisation de langages (de spécification et de programmation) dans les assistants de preuve

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.

Pour en savoir plus : http://gallium.inria.fr/~pdagand/
Séminaires
A Family of Tractable Graph Distances
Gestion de données du Web
Wednesday 04 July 2018 - 10h30
Salle : 465 - PCRI-N
Stratis Ioannidis .............................................

Binary pattern of length greater than 14 are abeli
Combinatoire
Friday 29 June 2018 - 14h30
Salle : 445 - PCRI-N
Matthieu Rosenfeld .............................................

Distributionally Robust Optimization with Principa
Optimisation combinatoire et stochastique
Friday 29 June 2018 - 11h00
Salle : 455 - PCRI-N
Dr. Jianqiang Cheng .............................................

Caractérisation de réseaux égocentrés par l'énumér
Friday 15 June 2018 - 14h30
Salle : 455 - PCRI-N
Raphaël Charbey .............................................

DATA VERACITY ASSESSMENT: HOW A-PRIORI KNOWLEDGE E
Intégration de données et de connaissances
Friday 15 June 2018 - 14h00
Salle : 445 - PCRI-N
Valentina Beretta .............................................