velus.bib

@inproceedings{JFLA17,
  title = {{V{\'e}rification de la g{\'e}n{\'e}ration modulaire du code imp{\'e}ratif pour Lustre}},
  author = {Bourke, Timothy and Dagand, Pierre-Evariste and Pouzet, Marc and Rieg, Lionel},
  url = {https://hal.inria.fr/hal-01403830},
  booktitle = {{JFLA 2017 - Vingt-huiti{\`e}me Journ{\'e}es Francophones des Langages Applicatifs}},
  address = {Gourette, France},
  year = 2017,
  month = jan,
  keywords = {Langages synchrones (Lustre) ;  Compilation ;  Assistants de Preuve (Coq)},
  pdf = {https://hal.inria.fr/hal-01403830/file/bourke%20%281%29.pdf},
  hal_id = {hal-01403830},
  hal_version = {v1},
  abstract = {
    Synchronous languages are used to program critical control applications.
    The Scade language, used in industry for these applications, is based on
    the Lustre language introduced by Caspi and Halbwachs. In this article
    we treat the formalization and proof, in the Coq proof assistant, of a
    key compilation pass: the translation of programs from Lustre into an
    imperative language. The challenge is to change from a synchronous
    dataflow semantics, where programs manipulate streams, to an imperative
    semantics, where the program manipulates memory sequentially. We specify
    and verify a simple code generator that treats core Lustre features:
    sampling, nodes, and delays. The proof uses an intermediate semantic
    model that mixes dataflow and imperative characteristics and allows the
    statement of an essential inductive invariant. We exploit this
    formalization to verify a classic optimization that fuses conditional
    structures in the generated imperative code.
  }
}

@inproceedings{PLDI17,
  title = {{A Formally Verified Compiler for Lustre}},
  author = {Bourke, Timothy and Brun, L{\'e}lio and Dagand, Pierre-Evariste and Leroy, Xavier and Pouzet, Marc and Rieg, Lionel},
  url = {https://hal.inria.fr/hal-01512286},
  booktitle = {{PLDI 2017 -  38th ACM SIGPLAN Conference on Programming Language Design and Implementation}},
  address = {Barcelone, Spain},
  organization = {{ACM}},
  year = 2017,
  month = jun,
  keywords = {Synchronous Languages (Lustre) ; Verified Compilation ; Interactive Theorem Proving (Coq)},
  pdf = {https://hal.inria.fr/hal-01512286/file/velus-pldi17.pdf},
  hal_id = {hal-01512286},
  hal_version = {v1},
  abstract = {
    The correct compilation of block diagram languages like Lustre, Scade,
    and a discrete subset of Simulink is important since they are used to
    program critical embedded control software. We describe the
    specification and verification in an Interactive Theorem Prover of a
    compilation chain that treats the key aspects of Lustre: sampling,
    nodes, and delays. Building on CompCert, we show that repeated execution
    of the generated assembly code faithfully implements the dataflow
    semantics of source programs.

    We resolve two key technical challenges. The first is the change from a
    synchronous dataflow semantics, where programs manipulate streams of
    values, to an imperative one, where computations manipulate memory
    sequentially. The second is the verified compilation of an imperative
    language with encapsulated state to C code where the state is realized
    by nested records. We also treat a standard control optimization that
    eliminates unnecessary conditional statements.
  }
}

@inproceedings{JFLA19,
  title = {{Clocked arguments in a verified Lustre compiler}},
  author = {Bourke, Timothy and Pouzet, Marc},
  url = {https://hal.inria.fr/hal-02005639},
  booktitle = {{JFLA 2019 - Les trenti{\`e}mes Journ{\'e}es Francophones des Langages Applicatifs}},
  address = {Les Rousses, France},
  series = {Les actes des trenti{\`e}mes Journ{\'e}es Francophones des Langages Applicatifs (JFLA 2019)},
  pages = 16,
  year = 2019,
  month = jan,
  pdf = {https://hal.inria.fr/hal-02005639/file/bourke-pouzet-jfla2019.pdf},
  hal_id = {hal-02005639},
  hal_version = {v1},
  abstract = {
    Lustre is a synchronous language for programming systems as block
    diagrams from which low-level imperative code is generated
    automatically. Recent work applies the Coq interactive proof assistant
    to specify a compiler from a core subset of Lustre to the Clight input
    language of CompCert from which assembly code is generated. The overall
    correctness proof connects the stream semantics of Lustre to the
    imperative semantics of the assembly code.

    Every stream in a Lustre program is associated with a static ‘clock’
    that represents when it is active. Compilation transforms the clocks
    into conditional statements that control when the corresponding value
    are calculated. Previous work made the simplifying assumption that the
    inputs and outputs of any given block shared the same static clock. This
    paper describes one way to lift this restriction. It requires enriching
    the static typing rules for clocks and the semantic model, and, to
    satisfy the Clight semantics, adding a compilation pass to ensure that
    any variable passed to a function call has been initialized.
  }
}

@inproceedings{SCOPES18,
  title = {{Towards a verified Lustre compiler with modular reset}},
  author = {Bourke, Timothy and Brun, L{\'e}lio and Pouzet, Marc},
  url = {https://hal.inria.fr/hal-01817949},
  booktitle = {{21st International Workshop on Software and Compilers for Embedded Systems (SCOPES 2018)}},
  address = {Sankt Goar, Germany},
  publisher = {{ACM Press}},
  series = {Proceedings of the 21st International Workshop on Software and Compilers for Embedded Systems (SCOPES 2018)},
  pages = 4,
  year = 2018,
  month = may,
  doi = {10.1145/3207719.3207732},
  keywords = {Compilers ; Formal software verification ; Semantics ; Synchronous Languages (Lustre) ; Verified Compilation},
  pdf = {https://hal.inria.fr/hal-01817949/file/paper.pdf},
  hal_id = {hal-01817949},
  hal_version = {v1},
  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.
  }
}

@article{POPL20,
  title = {{Mechanized semantics and verified compilation for a dataflow synchronous language with reset}},
  author = {Bourke, Timothy and Brun, L{\'e}lio and Pouzet, Marc},
  url = {https://hal.inria.fr/hal-02426573},
  journal = {{Proceedings of the ACM on Programming Languages}},
  publisher = {{ACM}},
  volume = {4},
  number = {POPL},
  pages = {1-29},
  year = {2020},
  month = jan,
  doi = {10.1145/3371112},
  keywords = {CCS Concepts: $\bullet$ Software and its engineering $\rightarrow$ Formal language definitions ; Software verification ; Compilers ; $\bullet$ Computer systems organization $\rightarrow$ Embedded software Additional Key Words and Phrases: stream languages ; verified compilation ; interactive theorem proving},
  pdf = {https://dl.acm.org/doi/pdf/10.1145/3371112?download=true&.pdf},
  hal_id = {hal-02426573},
  hal_version = {v1},
  abstract = {
    Specifications based on block diagrams and state machines are used to
    design control software, especially in the certified development of
    safety-critical applications. Tools like SCADE Suite and
    Simulink/Stateflow are equipped with compilers that translate such
    specifications into executable code. They provide programming languages
    for composing functions over streams as typified by Dataflow Synchronous
    Languages like Lustre.

    Recent work builds on CompCert to specify and verify a compiler for the
    core of Lustre in the Coq Interactive Theorem Prover. It formally links
    the stream-based semantics of the source language to the sequential
    memory manipulations of generated assembly code. We extend this work to
    treat a primitive for resetting subsystems. Our contributions include
    new semantic rules that are suitable for mechanized reasoning, a novel
    intermediate language for generating optimized code, and proofs of
    correctness for the associated compilation passes.
  }
}

@inproceedings{JFLA21,
  title = {Normalisation v{\'{e}}rifi{\'{e}}e du langage {Lustre}},
  author = {Timothy Bourke
		 and Paul Jeanmaire
		 and Basile Pesin
		 and Marc Pouzet},
  booktitle = {{JFLA 2021 - Les trente-deuxi{\`e}mes Journ{\'e}es Francophones des Langages Applicatifs}},
  pages = {117--133},
  year = 2021,
  month = apr,
  address = {Online},
  url = {https://hal.inria.fr/hal-03287572},
  pdf = {https://hal.inria.fr/hal-03287572/file/jfla.pdf},
  hal_id = {hal-03287572},
  hal_version = {v1},
  abstract = {
    Lustre is a synchronous dataflow language designed for programming
    embedded systems. In the Vélus project, we use Coq to develop and
    formalize a compiler that accepts a normalized form of the language and
    produces imperative code. While this restricted form is suitable for
    code generated from a user interface based on block diagrams, we wanted
    to allow programmers to use the complete language.

    In this article, we present the normalization pass that transforms the
    complete language into the normalized one. This transformation is
    divided into three steps so as to simplify the correctness proofs. To
    show that the semantics is preserved, it is necessary to prove that the
    three steps preserve certain static and dynamic properties of the
    language. In particular, the relation between the clock types and the
    dynamic semantic must be established.
  }
}

@article{EMSOFT21,
  author = {Timothy Bourke
		 and Paul Jeanmaire
		 and Basile Pesin
		 and Marc Pouzet},
  title = {Verified {Lustre} Normalization with Node Subsampling},
  journal = {ACM Transactions on Embedded Computing Systems},
  year = 2021,
  month = oct,
  volume = {20},
  number = {5s},
  pages = {Article 98},
  url = {emsoft2021/index.html},
  pdf = {https://hal.inria.fr/hal-03370264/file/paper.pdf},
  hal_id = {hal-03370264},
  hal_version = {v1},
  doi = {10.1145/3477041},
  note = {ESWEEK special issue including presentations at the 21st
		 Int. Conf. on Embedded Software (EMSOFT 2021)},
  abstract = {
    Dataflow languages allow the specification of reactive systems by
    mutually recursive stream equations, functions, and boolean activation
    conditions called clocks. Lustre and Scade are dataflow languages for
    programming embedded systems. Dataflow programs are compiled by a
    succession of passes. This article focuses on the normalization pass
    which rewrites programs into the simpler form required for code
    generation.

    Vélus is a compiler from a normalized form of Lustre to CompCert's
    Clight language. Its specification in the Coq interactive theorem prover
    includes an end-to-end correctness proof that the values prescribed by
    the dataflow semantics of source programs are produced by executions of
    generated assembly code. We describe how to extend Vélus with a
    normalization pass and to allow subsampled node inputs and outputs. We
    propose semantic definitions for the unrestricted language, divide
    normalization into three steps to facilitate proofs, adapt the clock
    type system to handle richer node definitions, and extend the end-to-end
    correctness theorem to incorporate the new features. The proofs require
    reasoning about the relation between static clock annotations and the
    presence and absence of values in the dynamic semantics. The
    generalization of node inputs requires adding a compiler pass to ensure
    the initialization of variables passed in function calls.
  }
}

@inproceedings{TYPES22,
  author = {Timothy Bourke
		 and Paul Jeanmaire
		 and Marc Pouzet},
  title = {Towards a denotational semantics of streams for a verified
		 {Lustre} compiler (short talk)},
  booktitle = {28th International Conference on Types for Proofs and
		 Programs},
  year = 2022,
  month = jun,
  address = {Nantes, France},
  url = {https://types22.inria.fr/files/2022/06/TYPES_2022_paper_28.pdf}
}

@inproceedings{JFLA23,
  title = {Analyse de d{\'{e}}pendance v{\'{e}}rifi{\'{e}}e pour
		 un langage synchrone {\`{a}} flot de donn{\'{e}}es},
  author = {Timothy Bourke
		 and Basile Pesin
		 and Marc Pouzet},
  pages = {101--120},
  booktitle = {{JFLA 2023 - Les trente-quatri{\`e}mes Journ{\'e}es
		 Francophones des Langages Applicatifs}},
  year = 2023,
  month = jan # {/} # feb,
  editor = {Timothy Bourke
		 and Delphine Demange},
  address = {Praz-sur-Arly, France},
  url = {jfla2023/index.html},
  pdf = {https://hal.inria.fr/hal-03936656/file/jfla23_paper_6388.pdf},
  hal_id = {hal-03936656},
  hal_version = {v1},
  abstract = {
    Vélus is a formalisation of a synchronous dataflow language and 
    compiler in the Coq proof assistant.
    It includes a definition of the source language's dynamic semantics,
    a compiler that produces imperative code,
    and an end-to-end proof that the compiler preserves the semantics of
    programs.

    In this article, we extend Vélus with the semantics of two activation
    structures that are provided by modern compilers:
    switchs and local declarations.
    These new constructions require adapting the static dependency analysis
    of Vélus, which produces an acyclic graph as a witness that a program is
    well formed.
    We use this witness to construct an induction schema and apply it to
    show, in Coq, that the semantic model is deterministic.
  }
}