Saved in:
| Main Authors: | , |
|---|---|
| Format: | Preprint |
| Published: |
2026
|
| Subjects: | |
| Online Access: | https://arxiv.org/abs/2606.01928 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866916072542699520 |
|---|---|
| author | Garoche, Pierre-Loïc Pesin, Basile |
| author_facet | Garoche, Pierre-Loïc Pesin, Basile |
| contents | Lustre is a synchronous dataflow language designed to implement safety-critical embedded software. In addition to writing executable programs, the language doubles as a program logic, used for writing specification as synchronous observers or assume-guarantee contracts that specify properties of these programs. These specifications may be used during testing or proved exhaustively using model-checking tools. We taught a course on Lustre to last year engineering students. To streamline the learning experience and avoid technical issues, we developped an online application, Learn-Heptagon, which allows for writing, simulating, and proving properties of Lustre programs. This paper presents the application and the associated lesson plan. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2606_01928 |
| institution | arXiv |
| publishDate | 2026 |
| record_format | arxiv |
| spellingShingle | Teaching Synchronous Dataflow Modelling with Learn-Heptagon Garoche, Pierre-Loïc Pesin, Basile Programming Languages Lustre is a synchronous dataflow language designed to implement safety-critical embedded software. In addition to writing executable programs, the language doubles as a program logic, used for writing specification as synchronous observers or assume-guarantee contracts that specify properties of these programs. These specifications may be used during testing or proved exhaustively using model-checking tools. We taught a course on Lustre to last year engineering students. To streamline the learning experience and avoid technical issues, we developped an online application, Learn-Heptagon, which allows for writing, simulating, and proving properties of Lustre programs. This paper presents the application and the associated lesson plan. |
| title | Teaching Synchronous Dataflow Modelling with Learn-Heptagon |
| topic | Programming Languages |
| url | https://arxiv.org/abs/2606.01928 |