Modular translation validation of a full-sized synchronous compiler using off-the-shelf verification tools (abstract)

Van Chan Ngo 1 Jean-Pierre Talpin 2 Thierry Gautier 2 Loic Besnard 3 Paul Le Guernic 2
1 ESTASYS - Efficient STAtistical methods in SYstems of systems
Inria Rennes – Bretagne Atlantique , IRISA-D4 - LANGAGE ET GÉNIE LOGICIEL
2 TEA - Tim, Events and Architectures
Inria Rennes – Bretagne Atlantique , IRISA-D4 - LANGAGE ET GÉNIE LOGICIEL
Abstract : The aim of this presentation is to demonstrate a scalable, modular, refinable methodology to design, assess and improve the trustability of an existing (20 years old), large (500k lines of C), open source (Eclipse/Polarsys IWG project POP) code generation suite using off-the-shelf, open-source, SAT/SMT verification tools (Yices), by adapting and optimizing the translation validation principle introduced by Pnueli et al. in 1998. This methodology results from the ANR project VERISYNC, in which we aimed at revisiting Pnueli's seminal work on translation validation using off-the-shelf, up-to-date, verification technology. In face of the enormous task at hand, the verification of a compiler infrastructure comprising around 500 000 lines of C code, we devised to narrow down and isolate the problem to the very data-structures manipulated by the infrastructure at the successive steps of code generation, in order to both optimize the whole verification process and make the implementation of a working prototype at all doable. Our presentation outlines the successive steps of this endeavour, from clock synthesis, static scheduling to target code production.
Type de document :
Communication dans un congrès
International Workshop on Software and Compilers for Embedded Systems, Jun 2015, St Goar, Germany. 〈http://www.scopesconf.org/scopes-15〉
Liste complète des métadonnées

Littérature citée [27 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01148919
Contributeur : Jean-Pierre Talpin <>
Soumis le : lundi 11 mai 2015 - 14:54:56
Dernière modification le : mercredi 11 avril 2018 - 02:01:16
Document(s) archivé(s) le : mercredi 19 avril 2017 - 20:50:16

Fichier

scopes15.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-01148919, version 1

Citation

Van Chan Ngo, Jean-Pierre Talpin, Thierry Gautier, Loic Besnard, Paul Le Guernic. Modular translation validation of a full-sized synchronous compiler using off-the-shelf verification tools (abstract). International Workshop on Software and Compilers for Embedded Systems, Jun 2015, St Goar, Germany. 〈http://www.scopesconf.org/scopes-15〉. 〈hal-01148919〉

Partager

Métriques

Consultations de la notice

302

Téléchargements de fichiers

130