L'insegnamento si propone di offrire agli studenti le conoscenze di base relative all'analisi ed alla verifica formale di 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 esposti la semantica operazionale e quella logica, basata sulla logica di Hoare. Infine si utilizzeranno alcuni tool per la sperimentazione pratica delle metodologie trattate.