Verifica automatica di programmi (2013/2014)

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 3-mar-2014 al 13-giu-2014.
Pagina Web
http://profs.sci.univr.it/~bonacina/teachingUniVR/VAP.html

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. 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 o solutori 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: eliminazione di quantificatori, 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)

Statistiche esiti
Esiti Esami Esiti Percentuali Media voti Deviazione Standard
Positivi 50.0% 28 0
Respinti --
Assenti --
Ritirati 50.0%
Annullati --
Distribuzione degli esiti positivi
18 19 20 21 22 23 24 25 26 27 28 29 30 30 e Lode
0.0% 0.0% 0.0% 0.0% 0.0% 0.0% 0.0% 0.0% 0.0% 0.0% 100.0% 0.0% 0.0% 0.0%

Valori relativi all'AA 2013/2014 calcolati su un totale di 2 iscritti. I valori in percentuale sono arrotondati al numero intero più vicino.