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