Předmět v sobě kombinuje několik témat - interaktivní a automatizované dokazování, sémantiku programovacích jazyků a dokazování korektnosti programů. Cílem se seznámit studenty s tím, jakým způsobem je možné pomocí softwarových nástrojů pro interaktivní a automatizované dokazování vytvářet formální počítačem ověřené důkazy korektnosti programů.
Existuje celá řada softwarových nástrojů, které umožňují interaktivně vytvářet důkazy, přičemž automaticky kontrolují správnost těchto důkazů a do určité míry umožňují automatizovat některé mechanické kroky důkazu.
První část semestru bude věnována primárně základům práce s jedním z takových softwarových nástrojů, se systémem Coq, který pak bude v další části semestru využíván pro dokazování korektnosti programů.
V této druhé části semestru budou probírána témata související s různými metodami dokazování této korektnosti. Aby bylo vůbec možné nějaké takové formální důkazy vytvářet, nejprve musí být formálně reprezentována sémantika programů. Část přednášek tedy bude věnovaná této problematice a také teorii typů, což je téma, které s výše uvedeným úzce souvisí. Dále pak budou studovány logiky používané pro dokazování vlastností programů - Hoarova logika a separační logika (což je modernější a obecnější rozšíření Hoarovy logiky o možnost dokazování korektnosti programů, které pracují s ukazateli a dynamicky alokovanými datovými strukturami).