Open AccessTowards a verified Lustre compiler with modular reset
Author(s) -
Timothy Bourke,
Lélio Brun,
Marc Pouzet
Publication year - 2018
Publication title -
hal (le centre pour la communication scientifique directe)
Language(s) - English
Resource type - Conference proceedings
DOI - 10.1145/3207719.3207732
Subject(s) - computer science , compiler , lustre (file system) , modular design , programming language , correctness , compiler correctness , sketch , construct (python library) , reset (finance) , operating system , algorithm , server , financial economics , economics
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.
Accelerating Research
Robert Robinson Avenue,
Oxford Science Park, Oxford
OX4 4GP, United Kingdom
Address
John Eccles HouseRobert Robinson Avenue,
Oxford Science Park, Oxford
OX4 4GP, United Kingdom