Il corso si propone di fornire una panoramica sulle tecniche di verifica formale applicate nell¿ambito del progetto di circuiti digitali, protocolli e software, con particolare enfasi al primo ambiente.
Tali tecniche hanno assunto un progressivo interesse ed applicazione come metodi complementari e/o alternativi alla simulazione, a causa della dimensione crescente dei sistemi progettati.
Il corso fornirà sia basi teoriche che esperienze applicative (uso di strumenti di verifica formale)

Verifica di proprietà logiche e temporali (model checking) e verifica di equivalenza per circuiti combinatori e sequenziali, theorem proving, linguaggi orientati alla verifica, manipolazioni simboliche mediante BDD, analisi di soddisfacibilità (SAT solving), interazioni tra verifica e testing, verifica di sistemi reattivi.