L'insegnamento si propone di fornire agli studenti le conoscenze di base relative all'analisi e alla verifica formale delle proprietà dei programmi. A questo scopo vengono introdotte le basi teoriche della modellazione e dell'analisi statica del comportamento dei programmi. Quindi sarà trattato un semplice linguaggio imperativo, di cui verranno esposte la semantica operazionale e quella logica, basata sulla logica di Hoare. Infine si utilizzeranno alcuni tool per la sperimentazione pratica delle metodologie trattate.