Content of the course

• formal aspects of testing (coverage criteria, software quality metrics)
  
• automated test generation: greybox fuzzing
• deductive verification (Dafny?)
• abstract interpretation
• points-to analysis, control and data dependencies, program slicing
• shape analysis via 3-valued logic (TVLA)
  
• symbolic execution, concolic execution, whitebox fuzz testing (SAGE)
• configurable program analysis (CPAchecker)
• verification via automata, symbolic execution, and Interpolation (UAutomizer)
• verification witnesses and SV-COMP
• SSA, bounded model checking, k-induction and k-inductive invariants, ?relation to backward symbolic execution?
  
• ?bonus: separation logic?
  

Examination

• oral 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 are worth to look in. Slides for each topic provide references to relevant sources. All these sources are available online or in study materials or in the faculty library. 

• E. M. Clarke, O. Grumberg, D. Kroening, D. Peled, and H. Veith: Model Checking (second edition), MIT Press, 2018.
  
• D. A. Peled: Software Reliability Methods, Springer, 2001.
• E. M. Clarke, T. A. Henzinger, H. Veith, and R. Bloem: Handbook of Model Checking, Springer, 2018.
  

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