Abstract
This lecture first studied the insertion of Esterel programs (or synchronous programs in general) into arbitrary execution environments, detailing the various ways in which events can be received or sent by an execution machine linking the locally synchronous world of Esterel and the asynchronous external world. He detailed the "exec" primitive for calling and managing asynchronous actions, originally introduced for robot control and already briefly introduced in the first lecture.
The lecture then looked at different ways of automatically proving properties of Esterel programs, building on the techniques presented in 2014-2016 for program verification: direct computations on explicit automata, implicit verification methods using SAT/SMT solvers, etc. Industrial examples illustrated the complementary nature of simulation and automatic proof development, highlighting the power of the latter approach.
