Course Unit Code | 460-4145/01 |
---|
Number of ECTS Credits Allocated | 4 ECTS credits |
---|
Type of Course Unit * | Optional |
---|
Level of Course Unit * | Second Cycle |
---|
Year of Study * | First Year |
---|
Semester when the Course Unit is delivered | Summer Semester |
---|
Mode of Delivery | Face-to-face |
---|
Language of Instruction | Czech |
---|
Prerequisites and Co-Requisites | Course succeeds to compulsory courses of previous semester |
---|
Name of Lecturer(s) | Personal ID | Name |
---|
| SAW75 | doc. Ing. Zdeněk Sawa, Ph.D. |
Summary |
---|
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). |
Learning Outcomes of the Course Unit |
---|
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. |
Course Contents |
---|
xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx |
Recommended or Required Reading |
---|
Required Reading: |
---|
[1] Benjamin C. Pierce et al. - Software Foundations (volumes 1 - 5). Electronic textbook, version 5.8., 2020. Dostupné na adrese https://softwarefoundations.cis.upenn.edu |
[1] Benjamin C. Pierce et al. - Software Foundations (volumes 1 - 5). Electronic textbook, version 5.8., 2020. Dostupné na adrese https://softwarefoundations.cis.upenn.edu |
Recommended Reading: |
---|
[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. |
[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.
|
Planned learning activities and teaching methods |
---|
Lectures, Tutorials |
Assesment methods and criteria |
---|
Task Title | Task Type | Maximum Number of Points (Act. for Subtasks) | Minimum Number of Points for Task Passing |
---|
Credit and Examination | Credit and Examination | 100 (100) | 51 |
Credit | Credit | 35 (35) | 20 |
Řešení zadaných problémů | Other task type | 15 | 7 |
Důkaz koreknosti zadaného programu | Project | 20 | 10 |
Examination | Examination | 65 | 30 |