Lecture: Verifiction with the Coq Proof Assistant
Organisation
Team
Lecturer: Prof. Dr. Annette Bieniusa
Assistant: Albert Schimpf, Elena Yanakieva
The lecture and course material will be in English.
Registration
Please register in the corresponding Olat course.
Exam
- To be announced
Objectives
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.