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 explicit 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 course IA169 System Verification and Assurance and  in a more detailed way in Chapter 8 of [CGKPV18] or Chapter 8 of [CHVB18]
• symbolic execution - explained in the course IA169 System Verification and Assurance and  in a more detailed way in [King76] available in study materials
  

Content of the course

The course presents only selected formal verification methods, in particular the basic methods not covered by the introductory course 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 take place in A318 on Mondays at 16:00.

Examination

• oral exam (either in person or 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 (infinished and 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.

There are also lectures recorded on spring 2020 and 2021. Note that these videos may not completely cover the lectures of 2023.