Skip to Main content Skip to Navigation
Conference papers

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.
Complete list of metadata

Cited literature [27 references]  Display  Hide  Download

https://hal.inria.fr/hal-01148919
Contributor : Jean-Pierre Talpin <>
Submitted on : Monday, May 11, 2015 - 2:54:56 PM
Last modification on : Friday, January 8, 2021 - 3:40:37 AM
Long-term archiving on: : Wednesday, April 19, 2017 - 8:50:16 PM

File

scopes15.pdf
Files produced by the author(s)

Identifiers

  • 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, ACM, Jun 2015, St Goar, Germany. ⟨hal-01148919⟩

Share

Metrics

Record views

430

Files downloads

192