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.
Type de document :
Communication dans un congrès
ACM Press. 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〉
Liste complète des métadonnées

https://hal.inria.fr/hal-01817949
Contributeur : Timothy Bourke <>
Soumis le : lundi 18 juin 2018 - 15:23:20
Dernière modification le : mercredi 20 juin 2018 - 01:02:46

Fichier

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

Identifiants

Collections

Citation

Timothy Bourke, Lélio Brun, Marc Pouzet. Towards a verified Lustre compiler with modular reset. ACM Press. 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〉

Partager

Métriques

Consultations de la notice

383

Téléchargements de fichiers

68