Lecture: Verifiction with the Coq Proof Assistant



Lecturer:  Prof. Dr. Annette Bieniusa

Assistant: Albert Schimpf, Elena Yanakieva

The lecture and course material will be in English.


Please register in the corresponding Olat course.


  • To be announced


After completing the module, students will be able to

  • understand the basic concepts of formal proofs, verification, and interactive theorem proving, and the role of proof assistants like Coq in this process.
  • use the Coq language to express formal models and their properties.
  • construct formal proofs, including reasoning about inductive and recursive definitions and usage of tactics and automation to simplify proofs.
  • verify the correctness of computer programs using Coq by reasoning about program semantics.