Verifica automatica di programmi (2012/2013)

Codice insegnamento
4S000023
Docente
Maria Paola Bonacina
Coordinatore
Maria Paola Bonacina
crediti
6
Settore disciplinare
ING-INF/05 - SISTEMI DI ELABORAZIONE DELLE INFORMAZIONI
Lingua di erogazione
Italiano
Periodo
II semestre dal 4-mar-2013 al 14-giu-2013.

Orario lezioni

II semestre
Giorno Ora Tipo Luogo Note
mercoledì 14.30 - 16.30 lezione Aula I  
venerdì 11.30 - 13.30 lezione Aula I  

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

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: chiusura di congruenza, liste, array, combinazione di procedure per condivisione di uguaglianze.

Testi di riferimento
Autore Titolo Casa editrice Anno ISBN Note
Daniel Kroening, Ofer Strichman Decision Procedures. An algorithmic point of view Springer 2008 978-3-540-74104-6
Aaron R. Bradley, Zohar Manna The Calculus of Computation - Decision Procedures with Applications to Verification (Edizione 1) Springer 2007 9783540741

Modalità d'esame

Esame mediante prove parziali:
Il voto è dato da 30% C1 + 35% C2 + 35% P, dove C1 è un compito scritto in classe (prova intermedia), C2 è un compito scritto (prova finale) in programma per il giorno del I appello della sessione estiva, e P è un progetto individuale. Il voto così generato viene registrato al I appello della sessione estiva.
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.
Non è possibile il "rifiuto" del voto: tutti i voti saranno registrati; lo studente può ritirarsi informando la docente. Tutti gli elaborati sono individuali; è vietato copiare o condividere codice o testo. Eventuali copiature determinano abbassamenti di voti per tutti gli studenti coinvolti.

Statistiche per i requisiti di trasparenza (Attuazione Art. 2 del D.M. 31/10/2007, n. 544)

I dati relativi all'AA 2012/2013 non sono ancora disponibili