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 de l'École normale supérieure, 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 <>
Submitted on : Monday, June 18, 2018 - 3:23:20 PM
Last modification on : Tuesday, May 4, 2021 - 2:06:02 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

594

Files downloads

493