Obiettivi formativi

L'insegnamento presenta problemi e metodi per l'analisi e la verifica di sistemi, mediante tecniche di ragionamento automatico quali dimostrazione automatica di teoremi applicata alla verifica deduttiva, o model checking.
Vi si impara a risolvere i problemi inerenti a esprimere il comportamento dei sistemi in formule logiche, e a progettare ragionatori automatici capaci di gestire tali formule in modo efficiente.

Programma

Procedure di prova in logica proposizionale e al primo ordine.
Teorie al primo ordine. Logica di Hoare, annotazioni, correttezza parziale e totale, stati, cammini, invarianti.
Generazione e prova di condizioni di verifica per la correttezza parziale e totale. Procedure di decisione per uguaglianza, strutture di dati, frammenti dell'aritmetica, e loro combinazione.

Modalità d'esame

Esame mediante prove parziali:
Il voto è dato da 30% C1 + 30% C2 + 40% P, dove C1 è la prova intermedia, C2 è la prova finale, e P è un progetto. Il voto così generato viene registrato al I appello della sessione di febbraio.
Esame senza prove parziali:
Il voto è dato da 100% E, dove E è un unico compito scritto, di difficoltà tale da uguagliare l'unione delle prove parziali.
Registrazione: non è previsto il rifiuto del voto e tutti i voti saranno registrati. Lo studente può ritirarsi informando la docente.
Tutti gli elaborati sono individuali. È vietato copiare o condividere codice o testo e le copiature determineranno abbassamenti di voti.