Learning materials (lecture slides, tutorial assignments, videos, script) for the course automatic software verification.

The course deals with approaches for automatic software verification. Topics of the course are:
- operational semantics of sequential programs
- configurable program analysis (including configuration of dataflow analyses and model checking)
- bounded model checking
- k-induction
- cooperative verification, especially conditional model checking


This seminar studies topics from our research area combination of validation of verification results. The goal of validation is to increase the trust in the validity of the result. Validation allows one to check that the verification was actually done and that the verification tool worked properly. In this seminar, we look into (1) protocols for validation, (2) validation techniques for several analyses like dataflow analysis, abstract interpretation, or model checking.

Under the guidance of your supervisor you will

  • use the given literature and search for additional literature to become acquainted with your topic,
  • prepare and give a presentation about your topic and afterwards discuss the topic with the other participants,
  • write a scientific report, which provides a summary of your topic.


Erste Veranstaltung: Dienstag, 20. April 2021, 14:00
Erste Veranstaltung: Montag, 12. April 2021, 14:25