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
Inria de Paris, DI-ENS - Département d'informatique de l'École normale supérieure, CNRS - Centre National de la Recherche Scientifique
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.
Liste complète des métadonnées

https://hal.inria.fr/hal-01817949
Contributor : Timothy Bourke <>
Submitted on : Monday, June 18, 2018 - 3:23:20 PM
Last modification on : Wednesday, February 20, 2019 - 3:33:06 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. ACM Press, pp.4, 2018, Proceedings of the 21st International Workshop on Software and Compilers for Embedded Systems (SCOPES 2018). 〈https://www.scopesconf.org/scopes-18/〉. 〈10.1145/3207719.3207732〉. 〈hal-01817949〉

Share

Metrics

Record views

453

Files downloads

103