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.