2025Activity reportProject-Team​​​‌PARKAS

4.1​​ Embedded Control Software

Embedded​​​‌ control software defines the​ interactions of specialized hardware​‌ with the physical world.​​ It normally ticks away​​​‌ unnoticed inside systems like​ medical devices, trains, aircraft,​‌ satellites, and factories. This​​ software is complex and​​​‌ great effort is required​ to avoid potentially serious​‌ errors, especially over many​​ years of maintenance and​​​‌ reuse.

Engineers have long​ designed such systems using​‌ block diagrams and state​​ machines to represent the​​​‌ underlying mathematical models. One​ of the key insights​‌ behind synchronous programming languages​​ is that these models​​​‌ can be executable and​ serve as the base​‌ for simulation, validation, and​​ automatic code generation. This​​​‌ approach is sometimes termed​ Model-Based Development (MBD). The​‌ SCADE language and associated​​ code generator allow the​​​‌ application of MBD in​ safety-critical applications. They incorporate​‌ ideas from Lustre,​​ Lucid Synchrone, and​​​‌ other programming languages.

4.2​ Hybrid Systems Design and​‌ Simulation

Modern embedded systems​​ are increasingly conceived as​​​‌ rich amalgams of software,​ hardware, networking, and physical​‌ processes. The terms Cyberphysical​​ System (CPS) or Internet-of-Things​​​‌ (IoT) are sometimes used​ as labels for this​‌ point of view.

In​​ terms of modeling languages,​​​‌ the main challenges are​ to specify both discrete​‌ and continuous processes in​​ a single hybrid language,​​​‌ give meaning to their​ compositions, simulate their interactions,​‌ analyze the behavior of​​ the overall system, and​​​‌ extract code either for​ target control software or​‌ more efficient, possibly online,​​ simulation. Languages like Simulink​​​‌ and Modelica are already​ used in the design​‌ and analysis of embedded​​ systems; it is more​​​‌ important than ever to​ understand their underlying principles​‌ and to propose new​​ constructs and analyses.

5.1 Awards

• Timothy Bourke‌ received an Outstanding Reviewer‌​‌ Award at the 21st​​ ACM/IEEE Embedded Systems Week​​​‌ in Taipei, Taiwan for‌ the EMSOFT conference.
• Timothy‌​‌ Bourke received a Distinguished​​ Reviewer Award at the​​​‌ 20th International Conference on‌ integrated Formal Methods, iFM‌​‌ 2025, in Paris, France.​​

6.1‌ Latest software developments

7.1‌ Verified compilation of Lustre‌​‌

Participants: Timothy Bourke,​​ Paul Jeanmaire, Balthazar​​​‌ Patiachvili, Marc Pouzet‌.

Vélus is a‌​‌ compiler for a subset​​ of Lustre and Scade​​​‌ that is specified in‌ the Coq 41 Interactive‌​‌ Theorem Prover (ITP). It​​ integrates the CompCert C​​​‌ compiler 34, 21‌ to define the semantics‌​‌ of machine operations (integer​​ addition, floating-point multiplication, etcetera)​​​‌ and to generate assembly‌ code for different architectures.‌​‌ The research challenges are​​ to

• to mechanize, i.e.,​​​‌ put into Coq, the‌ semantics of the programming‌​‌ constructs used in modern​​ languages for Model-Based Development;​​​‌
• to implement compilation passes‌ and prove them correct;‌​‌
• to interactively verify source​​ programs and guarantee that​​​‌ the obtained invariants also‌ hold of the generated‌​‌ code.

Work continued this​​ year on this long-running​​​‌ project by continuing to‌ develop a functional model‌​‌ for interactive verification, and​​ by experimenting with verified​​​‌ node inlining. The details‌ are described below. After‌​‌ his M2 internship, Balthazar​​ Patiachvili joined the team​​​‌ as a PhD student‌ working on arrays in‌​‌ verified compilers for dataflow​​ synchronous languages.

7.2​​​‌ Latency-based scheduling of synchronous‌ programs

Participants: Timothy Bourke‌​‌, Marc Pouzet,​​ Loïc Sylvestre.

External​​​‌ collaborators: Dumitru Potop Butucaru‌ (Inria) and; Matthieu Boitrel,‌​‌ Marc Brundler, Matthieu David,​​ Victor Jegu, Sylvain Sauvant,​​​‌ and Jean Souyris (Airbus).‌

Teams at Airbus have‌​‌ begun planning for the​​ next generation of flight​​​‌ control software. One of‌ their main aims is‌​‌ to enhance the existing​​ development process in two​​​‌ related ways: (i) by‌ providing new specification mechanisms‌​‌ that permit control engineers​​ to express application requirements​​​‌ more directly and with‌ more flexibility; (ii) by‌​‌ exploiting these mechanisms during​​ code generation to increase​​​‌ automation and better exploit‌ existing single-core and future‌​‌ multi-core computing units. We​​ have been working with​​​‌ them on language design‌ and compilation techniques for‌​‌ large synchronous specifications.

In​​ an approach termed “All-in-Lustre”,​​​‌ the top-level node of‌ a Lustre program is‌​‌ distinguished from inner nodes.​​ It contains special annotations​​​‌ to specify the triggering‌ and other details of‌​‌ node instances from which​​ separate “tasks” are to​​​‌ be generated. Special operators‌ are introduced to describe‌​‌ the buffering between top-level​​ instances. Notably, different forms​​​‌ of the when and‌ current operators are provided.‌​‌ Some of the operators​​ are under-specified and a​​​‌ constraint solver is used‌ to determine their exact‌​‌ meaning, that is, whether​​ the signal is delayed​​​‌ by zero, one, or‌ more cycles of the‌​‌ receiving clock, which depends​​ on the scheduling of​​​‌ the source and destination‌ nodes. Scheduling is formalized‌​‌ as a constraint solving​​ problem based on latency​​​‌ constraints between some pairs‌ of input/outputs that are‌​‌ specified by the designer.​​

This year, we continued​​​‌ experimenting with including the‌ allocation of tasks to‌​‌ cores within generated ILP​​ constraints. In our approach,​​​‌ inter-core communications within a‌ single cycle are forbidden,‌​‌ and additional synchronization instructions​​ are thus not needed.​​​‌ By improving the same‌ thread or different phase‌​‌ encoding and making better​​​‌ use of ILP-solver features,​ we managed to schedule​‌ the largest case study​​ in a more reasonable​​​‌ amount of time.

With​ Loïc Sylvestre , we​‌ started experimenting with the​​ CP-SAT solver included with​​​‌ Google's OR Tools. Since​ our problem is increasingly​‌ more combinatorial than linear,​​ it is natural to​​​‌ look at SAT-based constraint​ solvers. We experimented with​‌ a number of prototypes:​​ converting the LP format​​​‌ directly into a Python​ script, exploiting specific constraints​‌ for some forms, and​​ eliminating integer variables. Converting​​​‌ the LP format directly​ with some specific constraints​‌ gives quite promising results.​​ Despite time invested into​​​‌ eliminating integer variables, studying​ pseudo-boolean constraint encodings 29​‌, and experimenting with​​ MiniSat+, it is difficult​​​‌ to beat the lazy​ constraint generation of CP-SAT.​‌ We added more schedule​​ validation within the compiler,​​​‌ notably checking that dependency​ constraints are respected by​‌ external scheduling. The CP-SAT​​ solver can be tricky​​​‌ to compile and install,​ so we started developing​‌ an opam package to​​ make it a more​​​‌ reliable dependency for projects​ in OCaml.

For programs​‌ with many tasks running​​ at the fastest rate,​​​‌ the same thread or​ different phase approach is​‌ insufficient to obtain good​​ load balancing, since it​​​‌ prevents separating some producer-consumer​ pairs across different cores.​‌ We implemented a –base-barrier​​ option that inserts an​​​‌ additional synchronization barrier and​ allows the ILP solver​‌ to place fast tasks​​ before or after the​​​‌ barrier. This increases the​ combinatorial complexity of the​‌ constraint problem, but gives​​ better load balancing on​​​‌ the case-studies that we​ examined.

The constraint generation​‌ module in the presseail​​ compiler had become too​​​‌ complicated, so we restructured​ it to remove clustering​‌ (which ultimately proved ineffective)​​ and simplify the treatment​​​‌ of variables. We also​ included sample choices in​‌ the internal flowgraph representation​​ to facilitate the removal​​​‌ of redundant constraints, better​ validate schedules, and potentially​‌ allow for a finer-grained​​ causality analysis. We also​​​‌ introduced an explicit model​ for “unconstrained concomitance” and​‌ reworked options for eliminating​​ cycles.

We presented our​​​‌ work in a special-session​ on end-to-end latency in​‌ Cyber Physical systems at​​ the EMSOFT conference 16​​​‌ and started work on​ a joint proposal with​‌ collaborators in Germany.

Together​​ with our collaborators at​​​‌ Airbus and support from​ the transfer (Estelle Gaspard),​‌ legal (Manon Coger), and​​ financial (Odette Dabire) services​​​‌ of Inria Paris, we​ contributed to a project​‌ proposal on mixing control​​ algorithms and matrix manipulations​​​‌ within a dataflow synchronous​ language.

This work is​‌ funded by direct industrial​​ contracts with Airbus.

7.3 Sundials/ML​ interface for Zelus Runtime​‌

Participants: Timothy Bourke,​​ Alexandre Douard, Marc​​​‌ Pouzet.

Sundials 30​ is a collection of​‌ six numeric solvers. We​​ developed an OCaml interface​​ to this library 23​​​‌, 22 to better‌ understand it and to‌​‌ integrate it into the​​ runtime of the Zelus​​​‌ programming language. This interface‌ has been more difficult‌​‌ to maintain than expected​​ due to changes in​​​‌ OCaml 5.x, to introduce‌ the multi-threaded runtime, and‌​‌ to the Sundials library​​ itself, especially around the​​​‌ ARKode solver.

Previously, we‌ reported a behavior change‌​‌ in the OCaml 5.x​​ runtime which caused deadlocks​​​‌ in some of the‌ Sundials/ML examples. The suggested‌​‌ workaround was not completely​​ satisfying, but this year​​​‌ the OCaml runtime itself‌ was changed to avoid‌​‌ the problem we identified.​​ This allowed us to​​​‌ continue our work on‌ updating the interface. We‌​‌ first treated Sundials versions​​ 6.6.0 and 6.7.0. Then,​​​‌ with Alexandre Douard ,‌ during his summer L3‌​‌ internship, we treated version​​ 7.0.0 and almost completed​​​‌ 7.1.0. Alexandre Douard added‌ a test harness and‌​‌ worked especially on the​​ ARKode interface.

7.4 Semantics​​​‌ and Compilation of Arrays‌ in Dataflow Synchronous Languages‌​‌

Participants: Timothy Bourke,​​ Grégoire Bussone, Marc​​​‌ Pouzet.

The thesis‌ project of Gregoire Bussone‌​‌ studies the treatment of​​ arrays and state machines​​​‌ in synchronous languages, with‌ an emphasis on the‌​‌ generation of fast and​​ memory-efficient code, and eventual​​​‌ verification in a proof‌ assistant. The problem is‌​‌ essentially to transform a​​ functional input language where​​​‌ modifying an array element‌ creates a new array‌​‌ into sequential code with​​ in-place updates wherever possible.​​​‌ State machines are interesting‌ in this respect, due‌​‌ to the exclusive-or nature​​ of states: when states​​​‌ are always reset on‌ entry, they can share‌​‌ the same underlying memory.​​ Similarly, if a loop​​​‌ over an array is‌ reset at each instant,‌​‌ intermediate arrays need not​​ be stored as state​​​‌ variables.

This year we‌ studied the link between‌​‌ memory allocation and scheduling.​​ There are trade-offs between​​​‌ scheduling flexibility, copy minimization,‌ and compiler complexity. Certain‌​‌ operations, like array concatenation​​ and slices require special​​​‌ treatment. We proposed an‌ intermediate language that takes‌​‌ this into account and​​ defined its type systems​​​‌ and semantic models. The‌ MADL language, developed during‌​‌ Baptiste Pauget's PhD 36​​, addresses some of​​​‌ these aspects but not‌ node instances or conditional‌​‌ activation (clocks).

We also​​ worked on views,​​​‌ which allow some array‌ operations to be implemented‌​‌ as calculations on indexes​​ rather than memory modifications.​​​‌ For example, the reverse‌ function can be implemented‌​‌ by transforming an index​​ $i$ into $\mathrm{𝑠𝑖𝑧𝑒}-‌i$. This optimization‌ is difficult to apply‌​‌ in a modular manner.​​ We experimented with a​​​‌ compilation scheme that exploits‌ the traits of Rust‌​‌ to encode the index​​ transformations. The intermediate code​​​‌ requires a certain amount‌ of technical annotations, but‌​‌ the resulting assembly code​​ is compact and fast.​​​‌

We worked on the‌ forward and foreach loops‌​‌ that allow mixing dataflow​​ and array operators by​​​‌ alternating between streams of‌ arrays and arrays of‌​‌ streams. We also worked​​ on a new intermediate​​​‌ form for state machines‌ that generalizes the treatment‌​‌ of strong and weak​​​‌ transitions, and incorporates a​ static analysis based on​‌ when states are reset​​ to identify opportunities for​​​‌ sharing storage.

7.5 The​ Zelus Language

Participants: Timothy​‌ Bourke, Marc Pouzet​​, Gregoire Bussone.​​​‌

Zelus is our laboratory​ to experiment our research​‌ on programming languages for​​ hybrid systems. It is​​​‌ devoted to the design​ and implementation of systems​‌ that may mix discrete-time/continuous-time​​ signals and systems between​​​‌ those signals. It is​ first a synchronous language​‌ reminiscent of Lustre and​​ Lucid Synchrone with the​​​‌ ability to define functions​ that manipulate continuous-time signals​‌ defined by Ordinary Differential​​ Equations (ODEs) and zero-crossing​​​‌ events. The language is​ functional in the sense​‌ that a system is​​ a function from signals​​​‌ to signals (not a​ relation). It provides some​‌ features from ML languages​​ like higher-order and parametric​​​‌ polymorphism as well as​ dedicated static analyses.

7.6 A Constructive​​ Synchronous Semantics

Participants: Baptiste​​​‌ Pauget, Marc Pouzet‌.

External collaborators:Jean-Louis‌​‌ Colaco (ANSYS, Toulouse, France);​​ Michael Mendler (Univ. of​​​‌ Bamberg, Germany).

In 2024,‌ we have continued the‌​‌ development of ZRun. We​​ develop it in parallel​​​‌ with Zélus such that‌ every new programming construct‌​‌ (and more generally, any​​ language features) is implemented​​​‌ in both the compiler‌ and the interpreter.

The‌​‌ semantics is implemented as​​ an interpreter in a​​​‌ purely functional style, in‌ OCaml. The source code‌​‌ of this development is​​ available at the Zrun​​​‌ repository.

7.7 Translation‌ Validation Techniques for a‌​‌ Synchronous Language Compilers

Participants:​​ Timoty Bourke, Grégoire​​​‌ Bussone, Marc Pouzet‌.

Grégoire Bussone stated‌​‌ his PhD. in April​​ 2023. He studies the​​​‌ use of translation validation‌ techniques applied to a‌​‌ realistic synchronous language compiler.​​ The objective is to​​​‌ deal with the compilation‌ of array operations and,‌​‌ more generally, memory location.​​ Arrays are not supported​​​‌ in Vélus for the‌ moment. The problem is‌​‌ difficult and occurs in​​ two situations: avoid copies​​​‌ for functional iterators (e.g.,‌ map, fold, transpose, concat,‌​‌ reverse); optimize the representation​​ of the state in​​​‌ the final target code‌ (e.g., C) and avoid‌​‌ useless copies for states​​ whose lifetime never intersect​​​‌ (a classical situation that‌ comes for a Scade-like‌​‌ hierarchical automaton where all​​ states are entered by​​​‌ reset). For this work,‌ we follow a translation‌​‌ validation approach, relying on​​ an untrusted compiler and​​​‌ an independent but trustable‌ validation step. We also‌​‌ target a richer and​​ type-safe language back-end (here​​​‌ Rust) instead of C‌ to transmit some of‌​‌ the invariants from the​​ source. In the longer​​​‌ term, the purpose is‌ to be able to‌​‌ implement and to machine-check​​ the correctness of compilation​​​‌ techniques for a synchronous‌ language with arrays and‌​‌ their efficient compilation.

During​​ year 2023, several compilation​​​‌ steps that are implemented‌ in the Zélus compiler‌​‌ have been implemented as​​ translation validation functions proved​​​‌ correct in Coq, notably‌ the inlining, renaming, scheduling,‌​‌ normalization. Internally, the technique​​ employs the "locally nameless​​​‌ representation" introduced by Chargueraud.‌ The input language is,‌​‌ for the moment, a​​ simple subset of Zélus.​​​‌ The treatment of MADL‌ is under way.

7.8‌​‌ Verification by Abstract Interpretation​​​‌ of Synchronous Programs

Participants:​ Marc Pouzet, Charles​‌ De Haro, Xavier​​ Rival.

In Sept.​​​‌ 2024, Charles de Haro​ have started his PhD.​‌ thesis (Dir. Xavier Rival,​​ INRIA project team Antique;​​​‌ Marc Pouzet, INRIA project​ team Parkas) on the​‌ formal verification of synchronous​​ programs. The objective is​​​‌ to verify safety properties​ for programs that mix​‌ data-flow equations, hierarchical automata​​ and arrays. Those constructs​​​‌ are present in the​ industrial language Scade and​‌ the languages and compilers​​ developed at Parkas, namely​​​‌ Zélus and the Vélus​ compiler.

While previous works​‌ (in particular, Bertrand Jeannet​​ PhD. thesis, in 2000)​​​‌ have considered a subset​ of the language Lustre​‌ (a purely data-flow subset,​​ without clocks), the objective​​​‌ here is to deal​ with the mix with​‌ control structures, like the​​ by-case definition of streams​​​‌ and hierarchical automata, exploiting​ structural informations that is​‌ present in the source.​​ During first year, Charles​​​‌ have defined a new​ abstract semantics, reminiscent of​‌ the concrete, state-based semantics​​ presented at Emsoft'23 and​​​‌ implemented in the ZRun​ interpreter.

7.9 A Functional​‌ Semantics for Hybrid System​​ Simulation

Participants: Marc Pouzet​​​‌, Henri Saudubray.​

Modeling languages ​​for hybrid​‌ systems rely on a​​ specific runtime called a​​​‌ "simulation loop," which uses​ two auxiliary software components:​‌ a solver for the​​ numerical resolution of ordinary​​​‌ differential equations written in​ the Zelus source code,​‌ and a zero-crossing detection​​ algorithm. This loop is​​​‌ challenging to implement because,​ for the simulation to​‌ be as efficient as​​ possible, it is necessary​​​‌ to avoid copying arrays​ (which contain the velocities​‌ and positions defined in​​ the model) and to​​​‌ prevent unnecessary reinitializations of​ the solver.

With Henri​‌ Saudubray (M2 intern at​​ MPRI), we developed a​​​‌ precise formalization of this​ simulation loop, described as​‌ a Mealy machine in​​ a purely functional style​​​‌ (a pair s:S and​ a transition function of​‌ type f: S ->​​ A -> B *​​​‌ S). This leads to​ a first, purely functional​‌ description, parameterized by the​​ integration function given by​​​‌ the numerical solver and​ the zero-crossing detection function.​‌ The second version is​​ an imperative form deduced​​​‌ from the purely functional​ one where state modifications​‌ are done in place.​​ This leads to an​​​‌ effective implementation to be​ used, in the longer​‌ term, as the back-end​​ for Zélus. Ultimately, we​​​‌ want this simulation loop​ semantics to be added​‌ to the ZRun interpreter​​ in order to have​​​‌ an interpreter that handles​ the entirety of Zélus,​‌ including the hybrid part,​​ and that is independent​​​‌ of the compiler.

7.10​ What is a zero-crossing?​‌

Participants: Marc Pouzet,​​ Jean-Baptiste Jeannin, Jiawei​​​‌ Chen, Serra Dane​.

Most hybrid systems​‌ modeling languages ​​(e.g., Simulink,​​ Modelica), an Zélus is​​​‌ no exception rely on​ a zero-crossing detection algorithm.​‌ But what exactly does​​ it mean for a​​​‌ signal to cross zero,​ regardless of the algorithm​‌ that detects it, which​​ may not be complete​​​‌ (i.e., it may not​ detect that a signal​‌ crossed zero between two​​ time points)? This year,​​ we investigated this question​​​‌ by proposing a mathematical‌ definition independent of the‌​‌ algorithm used (in the​​ case of Zelus, we​​​‌ use a classical algorithm,‌ the Illinois method). This‌​‌ work has led to​​ a publication that will​​​‌ appear at NFM 2026‌ (NASA Formal Methods Symposium).‌​‌

7.11 Zélus with refinement​​ types

Participants: Marc Pouzet​​​‌, Jean-Baptiste Jeannin,‌ Jiawei Chen, Serra‌​‌ Dane.

The field​​ of functional programming languages​​​‌ ​​has developed significant work‌ on integrating dependent types‌​‌ by using a decision​​ algorithm to type programs.​​​‌ This allows properties of‌ the program to be‌​‌ expressed in the types​​ and to ensure that​​​‌ the program respects them‌ modularly. Several functional languages‌​‌ ​​have integrated these "refinement​​ types," notably, Liquid Haskell​​​‌ and F*.

Jean-Baptiste Jeannin‌ and his students aim‌​‌ to develop a version​​ of the Zélus language​​​‌ with "refinement types." We‌ are collaborating on this‌​‌ project. During the year,​​ Jiawei Chen, a doctoral​​​‌ student completing his thesis‌ on the subject, visited‌​‌ the team PARKAS several​​ times. Work is underway​​​‌ to define typing rules‌ for mutually recursive stream‌​‌ definitions and hierarchical automata,​​ based on the co-iterative​​​‌ semantics (EMSOFT'23). Some preliminary‌ works has been done‌​‌ for a simple case​​ of Zélus programs with​​​‌ ordinary differential equations. This‌ part will be presented‌​‌ this year, at NFM'26.​​

8.1‌ Bilateral contracts with industry‌​‌

9.1 International research‌ visitors

10.1 Promoting scientific activities​​

10.2​‌ Teaching - Supervision -​​ Juries - Educational and​​​‌ pedagogical outreach

• Marc Pouzet​ is Director of Studies​‌ for the CS department,​​ at ENS.
• Marc Pouzet​​​‌ and Timothy Bourke :​ “Parallélisme synchrone” au Master​‌ parisien de recherche en​​ informatique (MPRI; M2)
• Licence​​​‌ : Timothy Bourke :​ “Operating Systems” (L3), Lectures​‌ and TDs, ENS, France.​​
• Master: Marc Pouzet :​​​‌ “Synchronous Reactive Languages” (M2),​ Lectures, Master CPS (Cyber-physical​‌ Systems, led by Sergio​​ Mover (École Polytechnique).
• Master:​​​‌ Marc Pouzet "The Elements​ of Computing Systems". Cycle​‌ pluridisciplinaire d'études supérieures (CPES),​​ L2.
• Master: Timothy Bourke​​​‌ : “A Programmer’s introduction​ to Computer Architectures and​‌ Operating Systems" (M1), École​​ Polytechnique, France
• Master: Timothy​​​‌ Bourke presented lectures and​ TPs on Synchronous Languages​‌ in Carlos Agon's course​​ on concurrent models at​​​‌ Sorbonne Université.
• Bachelor: Timothy​ Bourke : “A Programmer’s​‌ introduction to Computer Architectures​​ and Operating Systems" (L2),​​​‌ École Polytechnique, France
• Marc​ Pouzet and Timothy Bourke​‌ organized and reviewed L3​​ and M1 internships at​​​‌ ENS DI.

10.3 Popularization​‌

11.1 Major​​​‌ publications

• 1 inproceedingsG.‌Guillaume Baudart, L.‌​‌Louis Mandel, E.​​Eric Atkinson, B.​​​‌Benjamin Sherman, M.‌Marc Pouzet and M.‌​‌Michael Carbin. Reactive​​ probabilistic programming.PLDI​​​‌ 2020 - 41th ACM‌ SIGPLAN International Conference in‌​‌ Programming Language Design and​​ ImplementationLondon / Virtual,​​​‌ United KingdomJune 2020‌HALDOI
• 2 inproceedings‌​‌T.Timothy Bourke,​​ V.Vincent Bregeon and​​​‌ M.Marc Pouzet.‌ Scheduling and Compiling Rate-Synchronous‌​‌ Programs with End-To-End Latency​​ Constraints.Leibniz International​​​‌ Proceedings in Informatics35th‌ Euromicro Conference on Real-Time‌​‌ Systems (ECRTS 2023)262​​35th Euromicro Conference on​​​‌ Real-Time Systems (ECRTS 2023)‌Vienna, AustriaJuly 2023‌​‌, 1:1--1:22HALDOI​​
• 3 inproceedingsT.Timothy​​​‌ Bourke, L.Lélio‌ Brun, P.-E.Pierre-Evariste‌​‌ Dagand, X.Xavier​​ Leroy, M.Marc​​​‌ Pouzet and L.Lionel‌ Rieg. A Formally‌​‌ Verified Compiler for Lustre​​.PLDI 2017 -​​​‌ 38th ACM SIGPLAN Conference‌ on Programming Language Design‌​‌ and ImplementationACMBarcelone,​​ SpainJune 2017HAL​​​‌
• 4 articleT.Timothy‌ Bourke, L.Lélio‌​‌ Brun and M.Marc​​ Pouzet. Mechanized semantics​​​‌ and verified compilation for‌ a dataflow synchronous language‌​‌ with reset.Proceedings​​ of the ACM on​​​‌ Programming Languages4POPL‌January 2020, 1-29‌​‌HALDOI
• 5 inproceedings​​T.Timothy Bourke,​​​‌ F.Francois Carcenac,‌ J.-L.Jean-Louis Colaço,‌​‌ B.Bruno Pagano,​​ C.Cédric Pasteur and​​​‌ M.Marc Pouzet.‌ A Synchronous Look at‌​‌ the Simulink Standard Library​​.EMSOFT 2017 -​​​‌ 17th International Conference on‌ Embedded SoftwareSeoul, South‌​‌ KoreaACM PressOctober​​ 2017, 23HAL​​​‌
• 6 inproceedingsT.Timothy‌ Bourke, J.-L.Jean-Louis‌​‌ Colaço, B.Bruno​​ Pagano, C.Cédric​​​‌ Pasteur and M.Marc‌ Pouzet. A Synchronous-based‌​‌ Code Generator For Explicit​​ Hybrid Systems Languages.​​​‌International Conference on Compiler‌ Construction (CC)LNCSLondon,‌​‌ United KingdomJuly 2015​​HAL
• 7 inproceedingsT.​​​‌Timothy Bourke, P.‌Paul Jeanmaire and M.‌​‌Marc Pouzet. Functional​​ Stream Semantics for a​​​‌ Synchronous Block-Diagram Compiler.‌LICS 2025 - 40th‌​‌ Annual ACM/IEEE Symposium on​​ Logic in Computer Science​​​‌Singapour, SingaporeJune 2025‌HAL
• 8 inproceedingsT.‌​‌Timothy Bourke, B.​​Basile Pesin and M.​​​‌Marc Pouzet. Verified‌ Compilation of Synchronous Dataflow‌​‌ with State Machines.​​ACM Transactions on Embedded​​​‌ Computing SystemsEMSOFT 2023:‌ 23rd International Conference on‌​‌ Embedded Software225s​​Hamburg, GermanySeptember 2023​​​‌, 137:1–137:26HALDOI‌
• 9 articleJ.-L.Jean-Louis‌​‌ Colaço, M.Michael​​ Mendler, B.Baptiste​​​‌ Pauget and M.Marc‌ Pouzet. A Constructive‌​‌ State-based Semantics and Interpreter​​ for a Synchronous Data-flow​​​‌ Language with State Machines:‌ Application to the Language‌​‌ Scade.ACM Transactions​​ on Embedded Computing Systems​​​‌ (TECS)225sSeptember‌ 2023, Article 152:‌​‌ 1-26HALDOI
• 10​​ inproceedingsL.Léonard Gérard​​​‌, A.Adrien Guatto‌, C.Cédric Pasteur‌​‌ and M.Marc Pouzet​​​‌. A modular memory​ optimization for synchronous data-flow​‌ languages: application to arrays​​ in a lustre compiler​​​‌.Proceedings of the​ 13th ACM SIGPLAN/SIGBED International​‌ Conference on Languages, Compilers,​​ Tools and Theory for​​​‌ Embedded SystemsBeijing, China​ACMJune 2012,​‌ 51--60HALDOI
• 11​​ incollectionJ. C.Juan​​​‌ Carlos Juega, S.​Sven Verdoolaege, A.​‌Albert Cohen, J.​​ I.José Ignacio Gómez​​​‌, C.Christian Tenllado​ and F.Francky Catthoor​‌. Patterns for parallel​​ programming on GPUs.​​​‌Patterns for parallel programming​ on GPUsEvaluation of​‌ State-of-the-Art Parallelizing Compilers Generating​​ CUDA Code for Heterogeneous​​​‌ CPU/GPU ComputingISBN 978-1-874672-57-9​Saxe-Cobourg2013HAL
• 12​‌ inproceedingsL.Louis Mandel​​, F.Florence Plateau​​​‌ and M.Marc Pouzet​. Static Scheduling of​‌ Latency Insensitive Designs with​​ Lucy-n.FMCAD 2011​​​‌ - Formal Methods in​ Computer Aided DesignAustin,​‌ TX, United StatesOctober​​ 2011HAL

11.2 Publications​​​‌ of the year

11.3​​ Cited publications

• 17 article​​​‌G.G .Berry.​ Real time programming: Special​‌ purpose or general purpose​​ languages.Information Processing​​​‌891989, 11-17​back to text
• 18​‌ articleA.Albert Benveniste​​, T.Timothy Bourke​​​‌, B.Benoit Caillaud​, J.-L.Jean-Louis Colaço​‌, C.Cédric Pasteur​​ and M.Marc Pouzet​​​‌. Building a Hybrid​ Systems Modeler on Synchronous​‌ Languages Principles.Proceedings​​ of the IEEE106​​​‌9September 2018,​ 1568 - 1592HAL​‌DOIback to text​​
• 19 articleA.Albert​​​‌ Benveniste, P.Paul​ Caspi, S.S.A.​‌ Edwards, N.Nicolas​​ Halbwachs, P. L.​​​‌P. Le Guernic and​ R.Robert de Simone​‌. The synchronous languages​​ 12 years later.​​​‌Proceedings of the IEEE​911January 2003​‌back to text
• 20​​ inproceedingsG.G. Berry​​. Real Time programming:​​​‌ Special purpose or general‌ purpose languages.IFIP‌​‌ CongressElsevier Science Publishers​​1989, 11--17back​​​‌ to text
• 21 inproceedings‌S.Sandrine Blazy,‌​‌ Z.Zaynah Dargaye and​​ X.Xavier Leroy.​​​‌ Formal Verification of a‌ C Compiler Front-End.‌​‌FM 2006: Int. Symp.​​ on Formal Methods4085​​​‌Lecture Notes in Computer‌ ScienceSpringer-Verlag2006,‌​‌ 460--475URL: http://gallium.inria.fr/~xleroy/publi/cfront.pdfback​​ to text
• 22 article​​​‌T.Timothy Bourke,‌ J.Jun Inoue and‌​‌ M.Marc Pouzet.​​ Sundials/ML: connecting OCaml to​​​‌ the Sundials numeric solvers‌.EPTCS2852018‌​‌, 101--130URL: http://www.tbrk.org/papers/abstracts.html#eptcs2018​​DOIback to text​​​‌
• 23 inproceedingsT.Timothy‌ Bourke, J.Jun‌​‌ Inoue and M.Marc​​ Pouzet. Sundials/ML: interfacing​​​‌ with numerical solvers.‌ACM Workshop on ML‌​‌ACMNara, JapanSeptember​​ 2016, URL: http://www.tbrk.org/papers/abstracts.html#ml16​​​‌back to text
• 24‌ inproceedingsT.Timothy Bourke‌​‌, B.Basile Pesin​​ and M.Marc Pouzet​​​‌. Verified Compilation of‌ Synchronous Dataflow with State‌​‌ Machines.EMSOFT 2023:​​ 23rd International Conference on​​​‌ Embedded Software225s‌Hamburg, GermanySeptember 2023‌​‌, 137:1--137:26HALDOI​​back to text
• 25​​​‌ inproceedingsP.Paul Caspi‌ and M.Marc Pouzet‌​‌. Synchronous Kahn Networks​​.ACM SIGPLAN International​​​‌ Conference on Functional Programming‌ (ICFP)Philadelphia, PensylvaniaMay‌​‌ 1996back to text​​
• 26 inproceedingsJ.-L.Jean-Louis​​​‌ Colaço, G.Grégoire‌ Hamon and M.Marc‌​‌ Pouzet. Mixing Signals​​ and Modes in Synchronous​​​‌ Data-flow Systems.ACM‌ International Conference on Embedded‌​‌ Software (EMSOFT'06)Seoul, South​​ KoreaOctober 2006back​​​‌ to text
• 27 inproceedings‌J.-L.Jean-Louis Colaço,‌​‌ B.Bruno Pagano and​​ M.Marc Pouzet.​​​‌ A Conservative Extension of‌ Synchronous Data-flow with State‌​‌ Machines.ACM International​​ Conference on Embedded Software​​​‌ (EMSOFT'05)Jersey city, New‌ Jersey, USASeptember 2005‌​‌back to text
• 28​​ inproceedingsJ.-L.Jean-Louis Colaço​​​‌, B.Bruno Pagano‌ and M.Marc Pouzet‌​‌. Scade 6: A​​ Formal Language for Embedded​​​‌ Critical Software Development.‌TASE 2017 - 11th‌​‌ International Symposium on Theoretical​​ Aspects of Software Engineering​​​‌Nice, FranceSeptember 2017‌, 1-10HALback‌​‌ to text
• 29 article​​N.Niklas Eén.​​​‌ Translating Pseudo-Boolean Constraints into‌ SAT.J. Satisfiability,‌​‌ Boolean Modelling and Computation​​21--4February 2006​​​‌, 1--26DOIback‌ to text
• 30 article‌​‌A.A.C. Hindmarsh,​​ P.P.N. Brown,​​​‌ K.K.E. Grant,‌ S.S.L. Lee,‌​‌ R.R. Serban,​​ D.D.E. Shumaker and​​​‌ C.C.S. Woodward.‌ SUNDIALS: Suite of Nonlinear‌​‌ and Differential/Algebraic Equation Solvers​​.ACM Transactions on​​​‌ Mathematical Software313‌September 2005, 363--396‌​‌back to text
• 31​​ thesisP.Paul Jeanmaire​​​‌. A denotational semantics‌ for a verified synchronous‌​‌ compiler.Université PSL​​ (Paris Sciences & Lettres)​​​‌December 2024HALback‌ to text
• 32 inproceedings‌​‌G.Gilles Kahn and​​ D. B.David B.​​​‌ MacQueen. Coroutines and‌ Networks of Parallel Processes‌​‌.IFIP Congress1977​​, 993-998back to​​​‌ text
• 33 inproceedingsG.‌Gilles Kahn. The‌​‌ semantics of a simple​​​‌ language for parallel programming​.IFIP 74 Congress​‌North Holland, Amsterdam1974​​back to text
• 34​​​‌ miscX.Xavier Leroy​. The Compcert verified​‌ compiler.2009,​​ URL: http://compcert.inria.fr/doc/index.htmlback to​​​‌ textback to text​
• 35 inproceedingsL.Louis​‌ Mandel and M.Marc​​ Pouzet. ReactiveML, a​​​‌ Reactive Extension to ML​.ACM International Conference​‌ on Principles and Practice​​ of Declarative Programming (PPDP)​​​‌LisboaJuly 2005back​ to text
• 36 phdthesis​‌B.Bapiste Pauget.​​ Memory Specification in a​​​‌ Data-flow Synchronous Language with​ Statically Sized Arrays.​‌PSL UniversitéParis, France​​December 2023back to​​​‌ text
• 37 incollectionC.​Christine Paulin-Mohring. A​‌ constructive denotational semantics for​​ Kahn networks in Coq​​​‌.From Semantics to​ Computer Science: Essays in​‌ Honour of Gilles Kahn​​Cambridge, UKCambridge University​​​‌ Press2009, 383--413​URL: https://hal.inria.fr/inria-00431806/documentback to​‌ text
• 38 phdthesisB.​​Basile Pesin. Verified​​​‌ Compilation of a Synchronous​ Dataflow Language with State​‌ Machines.PSL Research​​ UniversityOctober 2023,​​​‌ URL: https://velus.inria.fr/phd-pesin/thesis.pdfback to​ textback to text​‌
• 39 bookB. C.​​B. C. Pierce.​​​‌ Types and Programming Languages​.MIT Press2002​‌back to text
• 40​​ inproceedingsM.Mary Sheeran​​​‌. muFP, a language​ for VLSI design.​‌ACM Conference on LISP​​ and Functional ProgrammingAustin,​​​‌ Texas1984, 104-112​back to text
• 41​‌ miscThe Coq proof​​ Assistant.http://coq.inria.fr2019​​​‌back to text
• 42​ inproceedingsZ.Zhanyong Wan​‌ and P.Paul Hudak​​. Functional Reactive Programming​​​‌ from First Principles.​International Conference on Programming​‌ Language, Design and Implementation​​ (PLDI)2000back to​​​‌ text