author = {Albert Benveniste and Benoit Caillaud and Marc Pouzet},
  title = {The Fundamentals of Hybrid Systems Modelers},
  booktitle = {49th IEEE International Conference on Decision and Control (CDC)},
  year = 2010,
  address = {Atlanta, Georgia, USA},
  month = dec,
  url = {},
  doi = {10.1109/CDC.2010.5717614},
  abstract = {
      Hybrid systems modelers have become the corner stone of embedded
      system development, with Simulink a de facto standard and Modelica
      a new player. Such tools still raise a number of issues that, we
      believe, require more fundamental understanding.

     In this paper we propose using \emph{non standard analysis} as a
     semantic domain for hybrid systems --- non standard analysis is an
     extension of classical analysis in which infinitesimals (the
     $\varepsilon$ and $\eta$ in the celebrated generic sentence
     $\forall\ \varepsilon. \exists\ \eta \dots$ in college maths) can
     be manipulated as first class citizens. This allows us to provide a
     denotational semantics and a constructive semantics for hybrid systems,
     thus establishing simulation engines on a firm mathematical basis. In
     passing, we cleanly separate the job of the numerical analyst
     (solving differential equations) from that of the computer
     scientist (generating execution schemes).
  author = {Albert Benveniste and Timothy Bourke and
                 Benoit Caillaud and Marc Pouzet},
  title = {Divide and recycle: types and compilation for a 
                 hybrid synchronous language},
  booktitle = {ACM SIGPLAN/SIGBED Conference on Languages, Compilers,
		 Tools and Theory for Embedded Systems (LCTES'11)},
  month = apr,
  year = 2011,
  address = {Chicago, USA},
  url = {},
  doi = {10.1145/1967677.1967687},
  abstract = {
      Hybrid modelers such as Simulink have become corner stones of embedded
      systems development. They allow both \emph{discrete} controllers
      and their \emph{continuous} environments to be expressed \emph{in
      a single language}. Despite the availability of such tools,
      there remain a number of issues related to the lack of reproducibility
      of simulations and to the separation of the continuous part, which
      has to be exercised by a numerical solver, from the discrete part,
      which must be guaranteed not to evolve during a step.

      Starting from a minimal, yet full-featured, Lustre-like synchronous
      language, this paper presents a conservative extension where data-flow
      equations can be mixed with ordinary differential equations (ODEs)
      with possible reset. A type system is proposed to statically
      distinguish discrete computations from continuous ones and to ensure
      that signals are used in their proper domains. We propose a semantics
      based on \emph{non-standard analysis} which gives a synchronous
      interpretation to the whole language, clarifies the
      discrete/continuous interaction and the treatment of zero-crossings,
      and also allows the correctness of the type system to be established.

      The extended data-flow language is realized through a source-to-source
      transformation into a synchronous subset, which can then be compiled
      using existing tools into routines that are both efficient and bounded
      in their use of memory. These routines are orchestrated with a single
      off-the-shelf numerical solver using a simple but precise algorithm
      which treats causally-related cascades of zero-crossings. We have
      validated the viability of the approach through experiments with the
      SUNDIALS library.
  author = {Albert Benveniste and Timothy Bourke and
                 Benoit Caillaud and Marc Pouzet},
  title = {A Hybrid Synchronous Language with Hierarchical
		 Automata: Static Typing and Translation to Synchronous
  booktitle = {ACM SIGPLAN/SIGBED Conference on Embedded Software (EMSOFT'11)},
  month = oct,
  year = 2011,
  address = {Taipei, Taiwan},
  url = {},
  doi = {10.1145/2038642.2038664},
  abstract = {
      Hybrid modeling tools such as Simulink have evolved from simulation
      platforms into development platforms on which simulation, testing,
      formal verification and code generation are performed. It is thus
      critical to place them on a firm semantical basis where it can be
      proven that the results of simulation, compilation and
      verification are mutually consistent. Synchronous languages have
      addressed these issues but only for discrete systems. They cannot
      be used to model hybrid systems with both efficiency and

      Following the approach of Benveniste et al., we present the design of
      a hybrid modeler built from a synchronous language and an
      off-the-shelf numerical solver.  The main novelty is a language which
      includes control structures, such as hierarchical automata, for both
      continuous and discrete contexts.  These constructs can be arbitrarily
      mixed with data-flow and ordinary differential equations (ODEs).  A
      type system is required to statically ensure that all discrete state
      changes are aligned with zero-crossing events and that the function
      passed to the numerical solver is free of side-effects during
      integration. We show that well-typed programs can be compiled through
      a source-to-source translation into synchronous code which is then
      translated into sequential code using an existing synchronous language

      Based on the presented material, a compiler for a new synchronous
      language with hybrid features has been developed. We demonstrate its
      effectiveness on some examples.
  author = {Albert Benveniste and Timothy Bourke and Benoit
                 Caillaud and Marc Pouzet},
  title = {Non-Standard Semantics of Hybrid Systems Modelers},
  journal = {Journal of Computer and System Sciences},
  year = 2012,
  volume = 78,
  month = may,
  pages = {877--910},
  doi = {10.1016/j.jcss.2011.08.009},
  url = {},
  abstract = {
      Hybrid system modelers have become a corner stone of complex embedded
      system development. Embedded systems include not only control components
      and software, but also physical devices. In this area, Simulink is a de
      facto standard design framework, and Modelica a new player. However, such
      tools raise several issues related to the lack of reproducibility of
      simulations (sensitivity to simulation parameters and to the choice of
      a simulation engine).

      In this paper we propose using techniques from \emph{non-standard
      analysis} to define a semantic domain for hybrid systems. Non-standard
      analysis is an extension of classical analysis in which infinitesimal
      (the $\varepsilon$ and $\eta$ in the celebrated generic sentence
       $\forall\ \varepsilon\ \exists\ \eta\dots$ of college maths) can be
      manipulated as first class citizens. This approach allows us to define
      both a denotational semantics, a constructive semantics, and a Kahn
      Process Network semantics for hybrid systems, thus establishing
      simulation engines on a sound but flexible mathematical foundation.
      These semantics offer a clear distinction between the concerns of the
      numerical analyst (solving differential equations) and those of the
      computer scientist (generating execution schemes).

      We also discuss a number of practical and fundamental issues in hybrid
      system modelers that give rise to non reproducibility of results,
      nondeterminism, and undesirable side effects. Of particular importance
      are cascaded mode changes (also called ``zero-crossings'' in the
      context of hybrid systems modelers).
  visiblekey = {HSCC13},
  author = {Timothy Bourke and Marc Pouzet},
  title = {Zélus: A Synchronous Language with {ODEs}},
  booktitle = {16th International Conference on Hybrid Systems:
		 Computation and Control (HSCC'13)},
  pages = {113--118},
  month = mar,
  year = 2013,
  address = {Philadelphia, USA},
  url = {},
  abstract = {

	Zélus is a new programming language for modeling systems that
	mix discrete logical time and continuous time behaviors. From a
	user's perspective, its main originality is to extend an existing
	Lustre-like synchronous language with Ordinary Differential
	Equations (ODEs). The extension is conservative: any synchronous
	program expressed as data-flow equations and hierarchical automata
	can be composed arbitrarily with ODEs in \emph{the same source code}.

	A dedicated type system and causality analysis ensure that all
	discrete changes are aligned with zero-crossing events so that no
	side effects or discontinuities occur during integration. Programs
	are statically scheduled and translated into sequential code that,
	by construction, runs in bounded time and space. Compilation is
	effected by source-to-source translation into a small synchronous
	subset which is processed by a standard synchronous compiler
	architecture. The resultant code is paired with an off-the-shelf
	numeric solver.

	We show that it is possible to build a modeler for explicit hybrid
	systems \emph{à la Simulink/Stateflow} on top of an existing
	synchronous language, using it both as a semantic basis and as a
	target for code generation.
  visiblekey = {HSCC14},
  author = {Albert Benveniste and Timothy Bourke and Benoit Caillaud
		 and Bruno Pagano and Marc Pouzet},
  title = {A Type-Based Analysis of Causality Loops in Hybrid Modelers},
  booktitle = {17th International Conference on Hybrid Systems:
		 Computation and Control (HSCC'14)},
  pages = {71--82},
  month = apr,
  year = 2014,
  address = {Berlin, Germany},
  url = {},
  abstract = {
	Explicit hybrid systems modelers like \emph{Simulink/Stateflow}
	allow for programming both discrete- and continuous-time behaviors
	with complex interactions between them.  A key issue in their
	compilation is the static detection of algebraic or \emph{causality}
	loops. Such loops can cause simulations to deadlock and prevent the
	generation of statically scheduled code.

	This paper addresses this issue for a hybrid modeling language that
	combines synchronous data-flow equations with Ordinary Differential
	Equations (ODEs).  We introduce the operator last(x) for the
	left-limit of a signal $x$.  This operator is used to break
	causality loops and permits a uniform treatment of discrete and
	continuous state variables. The semantics relies on non-standard
	analysis, defining an execution as a sequence of infinitesimally
	small steps.  A signal is deemed \emph{causally correct} when it can
	be computed sequentially and only changes infinitesimally outside of
	announced discrete events like zero-crossings.  The causality
	analysis takes the form of a type system that expresses dependences
	between signals. In well-typed programs, signals are provably
	continuous during integration provided that imported external
	functions are also continuous.

	The effectiveness of this system is illustrated with several
	examples written in Zélus, a Lustre-like synchronous language
	extended with hierarchical automata and ODEs.

	See also: \url{}.
  author = {Timothy Bourke
		 and Jean-Louis Cola{\,{c}}o
		 and Bruno Pagano
		 and C{\'{e}}dric Pasteur
		 and Marc Pouzet},
  title = {A Synchronous-based Code Generator For Explicit Hybrid
		 Systems Languages},
  booktitle = {24th International Conference on Compiler Construction
		 (CC 2015)},
  year = 2015,
  pages = {to appear},
  address = {London, UK},
  month = apr,
  url = {},
  abstract = {
	Modeling languages for hybrid systems are cornerstones of embedded
	systems development in which software interacts with a physical
	environment. Sequential code generation from such languages is
	important for simulation efficiency and for producing code for
	embedded targets. Despite being routinely used in industrial
	compilers, code generation is rarely, if ever, described in full
	detail, much less formalized. Yet formalization is an essential
	step in building trustable compilers for critical embedded
	software development.

	This paper presents a novel approach for generating code from a
	hybrid systems modeling language. By building on top of an existing
	synchronous language and compiler, it reuses almost all the existing
	infrastructure with only a few modifications. Starting from an
	existing synchronous data-flow language conservatively extended with
	Ordinary Differential Equations (ODEs), this paper details the
	sequence of source-to-source transformations that ultimately yield
	sequential code. A generic intermediate language is introduced to
	represent transition functions. The versatility of this approach is
	exhibited by treating two classical simulation targets: code that
	complies with the FMI standard and code directly linked with an
	off-the-shelf numerical solver (Sundials CVODE).

	The presented material has been implemented in the Zélus compiler
	and the industrial Scade Suite KCG code generator of Scade 6.

	See also: \url{}.
  author = {Timothy Bourke
		   and Jun Inoue
		   and Marc Pouzet},
  title = {{Sundials/ML}: connecting {OCaml} to the {Sundials}
                   numeric solvers},
  publisher = {{Open Publishing Association}},
  journal = {Electronic Proceedings in Theoretical Computer Science},
  volume = 285,
  pages = {101--130},
  year = 2018,
  doi = {10.4204/EPTCS.285.4},
  note = {Extended version of paper appearing in the ACM Workshop on ML, 2016},
  abstract = {This paper describes the design and implementation of a
                  comprehensive OCaml interface to the Sundials
                  library of numeric solvers for ordinary differential
                  equations, differential algebraic equations, and
                  non-linear equations. The interface provides a
                  convenient and memory-safe alternative to using
                  Sundials directly from C and facilitates application
                  development by integrating with higher-level
                  language features, like garbage-collected memory
                  management, algebraic data types, and
                  exceptions. Our benchmark results suggest that the
                  interface overhead is acceptable: the standard
                  examples are rarely twice as slow in OCaml than in
                  C, and often less than 50\% slower. The challenges
                  in interfacing with Sundials are to efficiently and
                  safely share data structures between OCaml and C, to
                  support multiple implementations of vector
                  operations and linear solvers through a common
                  interface, and to manage calls and error signalling
                  to and from OCaml. We explain how we overcame these
                  difficulties using a combination of standard
                  techniques such as phantom types and polymorphic
                  variants, and carefully crafted data
  url = {}
  author = {Albert Benveniste and Benoit
                  Caillaud and Hilding Elmqvist and Khalil Ghorbal and Martin Otter and Marc Pouzet},
  title = {{Structural Analysis of Multi-Mode DAE Systems}},
  booktitle = {International Conference on
               Hybrid Systems: Computation and Control (HSCC)},
  year = 2017,
  month = {April 18-20},
  address = {Pittsburgh, USA},
  organization = {ACM},
  abstract = {Differential Algebraic Equation (DAE) systems constitute
                  the mathematical model supporting physical modeling
                  languages such as Modelica, VHDL-AMS, or
                  Simscape. Unlike ODEs, they exhibit subtle issues
                  because of their implicit latent equations and
                  related differentiation index. Multi-mode DAE (mDAE)
                  systems are much harder to deal with, not only
                  because of their mode-dependent dynamics, but
                  essentially because of the events and resets
                  occurring at mode transitions. Unfortunately, the
                  large literature devoted to the numerical analysis
                  of DAEs does not cover the multi-mode case. It
                  typically says nothing about mode changes. This lack
                  of foundations cause numerous difficulties to the
                  existing modeling tools. Some models are well
                  handled, others are not, with no clear boundary
                  between the two classes. In this paper we develop a
                  comprehensive mathematical approach to the
                  structural analysis of mDAE systems which properly
                  extends the usual analysis of DAE systems. We define
                  a constructive semantics based on nonstandard
                  analysis and show how to produce execution schemes
                  in a systematic way.},
  url = {}
  author = {Timothy Bourke and Francois Carcenac and Jean-Louis Cola\c{c}o
                  and Bruno Pagano and C\'edric Pasteur and Marc Pouzet},
  title = {{A Synchronous Look at the Simulink Standard Library}},
  booktitle = {ACM International Conference on Embedded Software (EMSOFT)},
  month = {October 15-20},
  address = {Seoul},
  year = 2017,
  abstract = {Hybrid systems modelers like
  Simulink come with a rich collection of discrete-time and
  continuous-time blocks. Most blocks are not defined in terms of more
  elementary ones---and some cannot be---but are instead written in
  imperative code and explained informally in a reference
  manual. This raises the question of defining a minimal set of
  orthogonal programming constructs such that
  most blocks can be \emph{programmed} directly and thereby given
  a specification that is mathematically precise, and whose compiled
  version performs comparably to handwritten code.
  In this paper, we show that a fairly large set of blocks from the
  Simulink standard library can be programmed in a precise, purely
  functional language using stream equations, hierarchical automata,
  Ordinary Differential Equations (ODEs), and deterministic
  synchronous parallel composition.  Some blocks cannot be expressed
  as they mix discrete-time and continuous-time signals in
  unprincipled ways and so are statically forbidden by the type

  The experiment is conducted in Z\'elus, a synchronous language that
  conservatively extends Lustre with constructs for
  programming systems that mix discrete-time and continuous-time signals.},
  url = {}
  author = {Guillaume Baudart},
  title = {{A Synchronous Approach to Quasi-Periodic Systems}},
  school = {\'Ecole normale sup\'erieure},
  year = 2017,
  address = {45 rue d'Ulm, 75230 Paris},
  abstract = {In this thesis we study embedded controllers implemented
                  as sets of unsynchronized periodic processes. Each
                  process activates quasi-periodically, that is,
                  periodically with bounded jitter, and communicates
                  with bounded transmission delays. Such reactive
                  systems, termed quasi-periodic, exist as soon as two
                  periodic processes are connected together. In the
                  distributed systems literature they are also known
                  as synchronous real- time models. We focus on
                  techniques for the design and analysis of such
                  systems without imposing a global clock
                  synchronization.  Synchronous languages were
                  introduced as domain specific languages for the
                  design of reactive systems. They offer an ideal
                  framework to program, analyze, and verify quasi-
                  periodic systems. Based on a synchronous approach,
                  this thesis makes contributions to the treatment of
                  quasi-periodic systems along three themes:
                  verification, implementation, and simulation.
                  Verification: The quasi-synchronous abstraction is a
                  discrete abstraction proposed by Paul Caspi for
                  model checking safety properties of quasi-periodic
                  systems. We show that this abstraction is not sound
                  in general and give necessary and sufficient
                  conditions on both the static communication graph of
                  the application and the real-time characteristics of
                  the architecture to recover soundness. We then
                  generalize these results to multirate systems.
                  Implementation: Loosely time-triggered architectures
                  are protocols designed to ensure the correct
                  execution of an application running on a
                  quasi-periodic system. We propose a unified
                  framework that encompasses both the application and
                  the protocol controllers. This framework allows us
                  to simplify existing protocols, propose optimized
                  versions, and give new correctness proofs. We
                  instantiate our framework with a protocol based on
                  clock synchronization to compare the performance of
                  the two approaches.  Simulation: Quasi-periodic
                  systems are but one example of timed systems
                  involving real-time characteristics and
                  tolerances. For such nondeterministic models, we
                  propose a symbolic simulation scheme inspired by
                  model checking techniques for timed automata. We
                  show how to compile a model mixing nondeterministic
                  continuous-time and discrete-time dynamics into a
                  discrete program manipulating sets of possible
                  values. Each trace of the resulting program captures
                  a set of possible executions of the source program.
  url = {}
  author = {Albert Benveniste and Timothy Bourke
                  and Beno\^{\i}t Caillaud and Jean-Louis Cola\c{c}o
                  and C\'edric Pasteur and Marc Pouzet},
  title = {{Building a Hybrid Systems Modeler on Synchronous
  Languages Principles}},
  journal = {Proceedings of the IEEE},
  year = 2018,
  abstract = { Hybrid systems modeling languages that mix discrete and
  continuous time signals and systems are widely used to develop
  Cyber-Physical systems where control software interacts with
  physical devices. Compilers play a central role, statically checking
  source models, generating intermediate representations for testing
  and verification, and producing sequential code for simulation and
  execution on target platforms.

  This paper presents a novel approach
  to the design and implementation of a hybrid systems language,
  built on synchronous language principles and their proven
  compilation techniques. The result is a hybrid systems modeling
  language in which synchronous programming constructs can be mixed
  with Ordinary Differential Equations (ODEs) and zero-crossing
  events, and a runtime that delegates their approximation to an
  off-the-shelf numerical solver.

  We propose an ideal semantics based
  on non standard analysis, which defines the execution of a hybrid
  model as an infinite sequence of infinitesimally small time
  steps. It is used to specify and prove correct three essential
  compilation steps: (1) a type system that guarantees that a
  continuous-time signal is never used where a discrete-time one is
  expected and conversely; (2) a type system that ensures the absence
  of combinatorial loops; (3) the generation of statically scheduled
  code for efficient execution.

  Our approach has been evaluated in
  two implementations: the academic language Zelus, which extends a
  language reminiscent of Lustre with ODEs and zero-crossing events,
  and the industrial prototype Scade Hybrid, a conservative extension
  of Scade 6.},
  url = {}
  author = {Albert Benveniste and
  Benoit Caillaud and Hilding Elmquist and Khalil Ghorbal and
  Martin Otter and Marc Pouzet},
  title = {Multi-Mode DAE Models - Challenges, Theory and
                  Implementation. },
  booktitle = {Computing and Software Science: state of the Art and
  editor = {Steffen B., Woeginger G.},
  publisher = {Springer},
  year = 2019,
  volume = 10000,
  series = {Lecture Notes in Computer Science},
  abstract = {Our objective is to model and simulate Cyber-Physical
                  Systems (CPS) such as robots, vehicles, and power
                  plants. The structure of CPS models may change
                  during simulation due to the desired operation, due
                  to failure situations or due to changes in physical
                  conditions. Corresponding models are called
                  multi-mode. We are interested in multi-domain,
                  component-oriented modeling as performed, for
                  example, with the modeling language Modelica that
                  leads naturally to Differential Algebraic Equations
                  (DAEs). This paper is thus about multi-mode DAE
                  systems. In particular, new methods are discussed to
                  overcome one key problem that was only solved for
                  specific subclasses of systems before: How to switch
                  from one mode to another one when the number of
                  equations may change and variables may exhibit
                  impulsive behavior? An evaluation is performed both
                  with the experimental modeling and simulation system
                  Modia, a domain specific language extension of the
                  programming language Julia, and with SunDAE, a novel
                  structural analysis library for multi-mode DAE
  author = {Guillaume Baudart and Louis Mandel and
    Eric Atkinson and Benjamin Sherman and Marc Pouzet and Michael Carbin},
  title = {{Reactive Probabilistic Programming}},
  booktitle = {International Conference on Programming Language Design and
               Implementation (PLDI)},
  year = 2020,
  month = {June 15-20},
  address = {London, United Kingdom},
  organization = {ACM},
  abstract = {
Synchronous modeling is at the heart of programming languages like
Lustre, Esterel, or Scade{} used routinely for implementing safety
critical control software, e.g., fly-by-wire and engine control in planes.
However, to date these languages have had limited modern support for
modeling uncertainty --- probabilistic aspects of the software's
environment or behavior --- even though modeling uncertainty is a
primary activity when designing a control system.

In this paper we present \ProbZelus the first {\em synchronous
probabilistic programming language}. 
ProbZelus conservatively provides the
facilities of a synchronous language to write control software, with
probabilistic constructs to model uncertainties and perform {\em

We present the design and implementation of the language. We propose a measure-theoretic semantics of probabilistic stream functions and a simple type discipline to
separate deterministic and probabilistic expressions. We demonstrate a
semantics-preserving compilation into a first-order functional language
that lends itself to a simple presentation of inference algorithms
for streaming models.
We also redesign the delayed sampling inference algorithm to provide
efficient \emph{streaming} inference.

Together with an evaluation on several reactive applications, our results
demonstrate that ProbZelus enables the design of reactive
probabilistic applications and efficient, bounded memory inference.},
  url = {}