Obiettivi formativi

L'insegnamento presenta problemi e metodi per l'analisi e la verifica di programmi, mediante tecniche di ragionamento automatico quali dimostrazione automatica di teoremi o model checking. Obbiettivo del corso è che lo studente, oltre a padroneggiare tecniche specifiche, comprenda i problemi inerenti da un lato a esprimere il comportamento dei programmi in formule logiche e dall'altro a progettare ragionatori automatici capaci di gestire tali formule in modo efficiente.

Programma

Dimostrazione automatica di teoremi in logica proposizionale e al primo ordine. Teorie al primo ordine. Logica di Hoare, annotazioni, correttezza parziale e totale, stati, cammini, invarianti. Generazione di invarianti. Tecniche di ragionamento automatico a scelta tra: procedure di decisione per la soddisfacibilità modulo teorie (uguaglianza, strutture di dati, combinazione di teorie, procedure di decisione basate su risoluzione e sovrapposizione); model checking (model checking simbolico, astrazione su predicati, raffinamento guidato da contro-esempi).

Modalità d'esame

Per gli studenti di CdLM/LS:
Esame mediante prove parziali: vale solo per il primo appello dopo la fine del corso. L'esame consta di un compito scritto (C) e di un progetto individuale (P) da realizzare a casa o in laboratorio durante il corso. Il voto d'esame è dato da: 50% C + 50% P.
Esame senza prove parziali: l'esame consta di un unico compito scritto (E), di difficoltà tale da uguagliare C+P, il cui voto determina il voto d'esame.
Registrazione: non è previsto il rifiuto del voto e tutti i voti saranno registrati. Lo studente insoddisfatto di come sta andando l'esame può ritirarsi non consegnando. Tutti gli elaborati sono individuali; è vietato copiare o condividere codice o testo. Eventuali copiature determineranno abbassamenti di voti.
Per gli studenti di DdR:
esame orale consistente nella presentazione di uno o più articoli dalla letteratura.