Il corso si propone di offrire agli studenti le conoscenze di base relative ai metodi logico matematici per l'analisi e la verifica formale di proprietà dei programmi. A questo scopo, dopo aver trattato di sistemi equazionali, riscrittura, logica e λ-calcolo, vengono introdotte le basi teoriche della semantica dei linguaggi di programmazione e della logica di Floyd-Hoare, nonché di alcune sue estensioni.

Il corso introduce all'uso di proof-assistant per l'analisi di programmi assistita da calcolatore, in particolare Agda.