Metodi formali

L'insegnamento intende esplorare le tecniche formali per migliorare l'affidabilità del software, con un focus particolare sulla specifica e dimostrazione di proprietà del software. Gli strumenti scelti sono i model checker simbolici e la della dimostrazione assistita dal calcolatore.

Lo studente sarà in grado di modellare e dimostrare la correttezza di semplici proprietà del software usando un insieme di tools presentati nelle ore di laboratorio.