The course is taught in English. Embedded systems, inclouding a mix of hardware and software and interacting continuously with the physical world, lie at the heart of the fourth industrial revolution, enabling unprecedented efficiency in mixed electronic, electrical and mechanical systems. Their effective implementation, in terms of performance, cost and energy, is thus essential to enable technological and economic progress in almost every domain of human activity. This course introduces the main mathematical models and methods used for the synthesis and verification of embedded hardware and software. It assumes a good knowledge of digital hardware design (with VHDL or Verilog) and of software implementation (with C, C++ or Java) for embedded systems, including a basic knowledge of microcontroller architectures and real-time operating systems. It provides the ability to select and use the best tools and methods for hardware/software co-design, as well as simulation and performance analysis. It provides knowledge about: - the SystemC language for mixed HW/SW modeling and verification, - synchronous languages for synthesis and verification of control-dominated embedded systems and - dataflow networks of synthesis and verification of data-dominated embedded systems.