Interaktivní a automatizované dokazování korektnosti programů

Přednášky:

1. Úvod. Funkcionální programování v systému Coq.
2. Důkazy indukcí. Práce s datovými strukturami.
3. Polymorfismus a funkce vyššího řádu.
4. Základy logiky v systému Coq. Používání taktik v důkazech.
5. Induktivně definovaná tvrzení. Dokazování vlastností relací.
6. Formalizace syntaxe a sémantiky jednoduchého imperativního jazyka.
7. Strukturální operační sémantika.
8. Ekvivalence programů.
9. Logiky pro dokazování vlastností programů: Hoarova logika a separační logika.
10. Typové systémy.
11. Dokazování vlastností typových systémů.
12. Dokazování vlastností funkcionálních programů.
13. Verifikace implementace datových struktur.

Cvičení:

1. Seznámení se se systémem Coq.
2. Základy funkcionálního programování v Coqu.
3. Jednoduché důkazy v systému Coq.
4. Základy logiky v systému Coq. Používání taktik v důkazech.
5. Další techniky důkazů v Coqu.
6. Formalizace syntaxe a sémantiky jednoduchého imperativního jazyka.
7. Formalizace sémantiky jednoduchého imperativního jazyka v Coqu.
8. Dokazování některých vlastností programů.
9. Formalizace Hoarovy logiky v Coqu, důkaz korektnosti konkrétního jednoduchého algoritmu.
10. Další důkazy korektnosti algoritmů pomocí Hoarovy logiky.
11. Formalizace jednoduchého typového systému v Coqu.
12. Dokazování vlastností funkcionálních programů.
13. Verifikace implementace datových struktur.