To fully understand the lessons, students should be familiar with the following topics:

• basic terms of formal language theory: an alphabet, a word, a (formal) language, etc.
• languages over infinite words and Büchi automata - see Section 9.1 of [CGP99] or Chapter 5 of [Pel01]
• Linear Temporal Logic (LTL) - see Chapter 3 of [CGP99] or Chapter 5 of [Pel01]
• automata-based LTL Model Checking - see Chapter 9 of [CGP99] or Chapter 6 of [Pel01]

The course will not cover all areas of formal verification. For example, we will not elaborate on these topics:

• symbolic model checking - briefly explained in the courses IV113 Introduction to Validation and Verification and IA169 System Verification and Assurance, and  in a more detailed way in Chapter 6 of [CGP99]
• bisimulation equivalence and equivalence checking - explained in the course IA006 Selected Topics on Automata Theory and in Chapter 8 of  [Pel01]
• runtime verification

Where:

• [CGP99] stands for the book E. M. Clarke, O. Grumberg, and D. A. Peled: Model Checking, MIT Press, 1999 (available in FI library), and 
• [Pel01] stands for the book D. A. Peled: Software Reliability Methods, Springer, 2001 (available in FI library).

Examination:

• oral exam
• no intrasemestral tests, no written exams, no mandatory homeworks