The course combines several topics - interactive and automated theorem proving, semantics of programming languages and proving correctness of programs. The aim is to introduce to students the possibilities of the use of software tools for interactive and automated theorem proving for construction of formal proofs, verified by a computer, of correctness of programs.
There exists a lot of software tools that allow an interactive construction of proofs, where the correctness of these proofs is checked automatically, and that to automate, to a certain degree, some mechanical steps of these proofs.
The first part of a semester will be devoted primarily to the basics of working with one of such tools, with Coq proof assistant, which will be used in the second part of a semester for proving correctness of programs.
In this second part of semester we will discuss topics concerning different methods of proving of this correctness. To allow to create such formal proofs, a semantics of programs must be formally represented at first. So some lectures will deal with this topic and also with theory of types, which is a closely connected topic. Other discussed topic will be logics used for proving properties of programs - Hoare logic and separation logic (which is a modern and more general extension of Hoare logic that allows to prove correctness of programs that work with pointers and dynamically allocated data structures).