Lecture: 2.01.489 Automated Program Verification - Details

Lecture: 2.01.489 Automated Program Verification - Details

You are not logged into Stud.IP.

General information

Course name Lecture: 2.01.489 Automated Program Verification
Subtitle inf489 / inf803
Course number 2.01.489
Semester WiSe24/25
Current number of participants 14
expected number of participants 100
Home institute Department of Computing Science
Courses type Lecture in category Teaching
Next date Thursday, 14.11.2024 10:00 - 12:00, Room: A01 0-006
Type/Form VL+Ü
Lehrsprache deutsch und englisch

Rooms and times

A01 0-008
Tuesday: 10:00 - 12:00, weekly (14x)
A01 0-006
Thursday: 10:00 - 12:00, weekly (12x)

Module assignments

Comment/Description

This course offers a hands-on introduction to the usage, construction, and theory of automated deductive program verifiers. Students should acquire the skills to apply and extend tool-supported methodologies for developing proven-correct software. The course will intermix theoretical content with hands-on experience.

# Content
The course covers reasoning principles, technologies, and engineering aspects underlying automated deductive verification tools. In particular, it introduces
1. program logics for writing formal correctness proofs (for example weakest preconditions and separation logic);
2. SMT solvers (for example Z3) for automating reasoning about logical formulas;
3. intermediate verification languages (for example Viper) for encoding verification methodologies; and
4. source code verifiers for handling feature-rich programming languages.

# Learning objectives
A student who has met the objectives of the course will be able to:
  • specify functional correctness properties of imperative programs;
  • use automated verification tools to develop formally verified software;
  • justify why a program meets its specification based on sound reasoning principles;
  • explain the technology stack involved in building automated verification tools;
  • compare deductive program verification to other methods aiming at increasing confidence in software correctness;
  • encode verification-related decision problems to SMT (satisfiability modulo theories);
  • identify potential bottlenecks in existing SMT encodings; and
  • construct methodologies for program verification problems and justify the involved design decisions.

# Literature
All relevant material (lecture notes, slides, videos, exercises, etc.) will be made available online.