460-4145/01 – Interactive and Automated Proving of Program Correctness (IADKP)

In this course, students will get acquainted with methods for formal proving correctness of programs and with a use of tools for interactive and automated theorem proving that can be used for this purpose. The aim is to learn how a semantics of programming languages can be formalized and how properties of programs can be formalized and proved using tools as Hoare logic, separation logic and theory of types.Students will learn how such tools can be formalized and implemented using software tools such as, for example, Coq proof assistant that can be used for partially automated creation of proof and automated verification of correctness of these proofs.

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).

[2] Yves Bertot, Pierre Castéran - Interactive Theorem Proving and Program Development, Springer, 2004. [3] Andrew W. Appel et al. - Program Logics for Certified Compilers, Cambridge University Press, 2014. [4] Adam Chlipala - Certified Programming with Dependent Types: A Pragmatic Introduction to the Coq Proof Assistant. The MIT Press, 2013. [5] Benjamin C. Pierce - Types and Programming Languages, MIT Press, 2002. [6] Benjamin C. Pierce, ed. - Advanced Topics in Types and Programming Languages. MIT Press, 2004. [7] Glynn Winskel - Formal Semantics of Programming Languages, The MIT Press, 1993. [8] Hans Hüttel - Transitions and Trees: An Introduction to Structural Operational Semantics, Cambridge University Press, 2010.

V průběhu semestru studenti vypracovávají řešení zadaných úloh v programu Coq. Na závěr semestru vypracují v programu Coq kompletní důkaz korektnosti nějakého zadaného algoritmu. Předmět je zakončen zkouškou, která se skládá z písemné a ústní části.