Preliminaries

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 Sections 7.2-7.6 of [CGKPV18] or Section 4.2 of [CHVB18] or Chapter 5 of [Pel01]
• Linear Temporal Logic (LTL) - see Chapter 4 of [CGKPV18] or Chapter 5 of [Pel01] or Section 2.3 of [CHVB18]
  
• automata-based LTL Model Checking - see Sections 7.7-7.11 of [CGKPV18] or Chapter 6 of [Pel01] or Chapter 5 of [CHVB18]
• symbolic model checking - explained in the courses IV113 Introduction to Validation and Verification and IA169 System Verification and Assurance, and  in a more detailed way in Chapter 8 of [CGKPV18] or Chapter 8 of [CHVB18]

Content of the course

The course presents only selected formal verification methods, in particular the basic methods not covered by introductory courses IV113 Introduction to Validation and Verification and IA169 System Verification and Assurance and some recent advanced methods. Still there are many topics not covered by any of the mentioned courses, for example:

• bisimulation equivalence and equivalence checking - explained in the course IA006 Selected Topics on Automata Theory and in Chapter 11 [CGKPV18] or Chapter 8 of  [Pel01]
• runtime verification

Lectures

The lectures have the form of a teleconference via Zoom.

Examination

• oral exam via a videocall, students can use slides, papers, and books during the exam
  
• no intrasemestral tests, no written exams, no mandatory homeworks

Literature

There is no single book covering all topics of this course. However, the following books (mostly mentioned above) are worth to look in and the lecture notes (never finished and already slightly obsolete) cover some of the topic. Slides for each topic provide references to relevant sources. All these sources are available online or in study materials or in the faculty library. 

• [CGKPV18] stands for the book E. M. Clarke, O. Grumberg, D. Kroening, D. Peled, and H. Veith: Model Checking (second edition), MIT Press, 2018. (available in FI library)
  
• [Pel01] stands for the book D. A. Peled: Software Reliability Methods, Springer, 2001. (available in FI library)
• [CHVB18] stands for the book E. M. Clarke, T. A. Henzinger, H. Veith, and R. Bloem: Handbook of Model Checking, Springer, 2018. (available in FI library)

• Andreas Zeller: The Debugging Book (Tools and Techniques for Automated Software Debugging), 2021.