Verification of Reactive Systems

The course introduces abstract models for concurrent, reactive, non-terminating systems which are used for verification purposes. Various concepts of correctness in terms of equivalence or compliance with formal properties expressed in a temporal logic are considered. Algorithm verifying equivalence or compliance are analysed with respect to their complexity. During the second part of the course the students will use software tools to verify simple systems.

A good understanding of
- how concurrent, reactive, non-terminating systems can be verified and
- how model checker tools work and what are their limits.
Familiarity with at least two Model Checker tools.