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 programmi e della logica di Floyd-Hoare. Inoltre saranno introdotte tecniche di analisi statica di programmi con puntatori basate sulla Separation logic.