This is a course for MSc and PhD students in Computer Science.

The course focuses on reactive synthesis, the automatic generation of a system from its temporal logic specification. The topics we will cover include: temporal logics syntax and semantics, automata over infinite words, infinite games, symbolic representations and BDDs, general reactivity of rank (1) games. We will further cover the Spectra language and recent research results from the SYNTECH project: http://smlab.cs.tau.ac.il/syntech/

Class attendance is mandatory.  The final grade is based on a combination of homework exercises, final project and/or final home exam.  

Related topics/courses: logic, formal verification, automata and formal languages, software engineering