Skip to Main content Skip to Navigation
Conference papers

Towards a verified Lustre compiler with modular reset

Timothy Bourke 1, 2, 3 Lélio Brun 1, 2, 3 Marc Pouzet 1, 2, 4, 3 
1 Parkas - Parallélisme de Kahn Synchrone
DI-ENS - Département d'informatique - ENS Paris, CNRS - Centre National de la Recherche Scientifique, Inria de Paris
Abstract : This paper presents ongoing work to add a modular reset construct to a verified Lustre compiler. We present a novel formal specification for the construct and sketch our plans to integrate it into the compiler and its correctness proof.
Complete list of metadata

Cited literature [8 references]  Display  Hide  Download

https://hal.inria.fr/hal-01817949
Contributor : Timothy Bourke Connect in order to contact the contributor
Submitted on : Monday, June 18, 2018 - 3:23:20 PM
Last modification on : Wednesday, June 8, 2022 - 12:50:04 PM

File

paper.pdf
Files produced by the author(s)

Identifiers

Collections

Citation

Timothy Bourke, Lélio Brun, Marc Pouzet. Towards a verified Lustre compiler with modular reset. 21st International Workshop on Software and Compilers for Embedded Systems (SCOPES 2018), May 2018, Sankt Goar, Germany. pp.4, ⟨10.1145/3207719.3207732⟩. ⟨hal-01817949⟩

Share

Metrics

Record views

160

Files downloads

230