To the German version

Formal Specification and Verification 2



This lecture covers advanced topics of formal specification and verification. It builds on the topics covered in the lecture "Formale Spezifikation und Verifikation 1" of the BSc-course.


There is no lecture on 31.10.2017 (holiday).

Detailed Time Table

Date Lecturer Planned Topics
17.10. DB + MH Organization, Introduction to lecture + lattices
24.10. DB Dataflow analysis: Control-flow automata (CFAs) + Configurable program analyses (CPAs)
31.10.  -  No lecture
07.11. DB Abstract domains (reaching definitions, intervals, values)
14.11. DB Counterexample-guided abstraction refinement (CEGAR) + Lazy abstraction
21.11. DB Interpolation, Invariant synthesis
28.11. DB Impact, predicate abstraction, k-induction, bounded model checking
05.12. MH Interprocedural analysis
12.12. MH Type systems
19.12. MH Satisfiability modulo theories (SMT)
09.01. MH IC3: Symbolic model-checking with BDDs, IC3 algorithm, proofs of correctness and completeness
16.01. MH Timed automata
23.01. DB Technology: Witnesses, Visualization, Tools for Software Verification
30.01. MH Hybrid automata (generalization of timed automata: arbitrary continuous variables)
06.02. MH Generalizing counterexamples: certification of temporal properties with parity games

DB: Prof. Dr. Dirk Beyer
MH: Prof. Martin Hofmann, PhD


Learning Material

Copyright applies to the following learning material. Attendees of the lecture are permitted to use the material for their personal studies. All other rights are reserved.

Target Audience

MSc Computer Science (Informatik). Participants may take part in the joint training course (Praktikum) offered.


Training (Praktikum)

A joint training course (Praktikum) is available. The training starts in the middle of the semester.


Useful Links