Introduction to program verification

Francesco Ranzato
Department of Mathematics, University of Padua

Program verification is the act of proving or disproving the correctness of a given program with respect to a given specification of a program property, using a precise model for the program behaviour, a precise language for expressing program specifications and a verification algorithm. Program verification is very helpful for automatically detecting program bugs, one of the worst enemies of software engineers. Program verification relies on static program analysis, that is the analysis of computer software which is performed without actually executing programs. The aims of this "Introduction to program verification" crash course are: (1) to describe why program verification is important in practice; (2) to provide at least an informal introduction to the basic techniques used for designing a static program analysis; (3) to use some verification and analysis tools in practice.

- Program semantics
- Static program analysis and verification
- Tools for software verification

Course requirements
Basic knowledge of programming

Examination and grading

To be defined

To be defined
<< Courses in 2017-2018