Reactive systems, such as concurrent programs, communication protocols and control systems, are characterized by their non-terminating behavior and their persistent interaction with their environment. This course introduces the theory and practice of formal methods for the design and analysis of reactive systems. The emphasis is on the underlying logical and automata-theoretic concepts, the algorithmic solutions, and heuristics to cope with the high computational complexity.
|SSC1||Examination of the state of the art to identify research problems related to the design, construction, use and evaluation of complex software-intensive sociotechnical systems||S|
|SSC5||Contribution of solutions to open problems related to software verification and validation applications and methods, techniques and tools||A|
|Code||Learning Outcome||Associated competences||Proficiency level|
|RA-AV-1||Familiarity with the idea of design and implementation requirement||SSC1,SSC5||S|
|RA-AV-4||Knowledge of techniques for proving code correctness||SSC1,SSC5||A|
Subject learning guide for Formal Methods for Concurrent and Reactive Systems