Verifica (2009/2010)

Codice insegnamento
4S02800
Docente
Maria Paola Bonacina
Coordinatore
Maria Paola Bonacina
crediti
6
Settore disciplinare
ING-INF/05 - SISTEMI DI ELABORAZIONE DELLE INFORMAZIONI
Lingua di erogazione
Inglese
Periodo
II semestre dal 1-mar-2010 al 15-giu-2010.
Pagina Web
http://profs.sci.univr.it/~bonacina/teachingUniVR/Verifica2009-10.html

Orario lezioni

II semestre
Giorno Ora Tipo Luogo Note
martedì 14.30 - 16.30 lezione Aula I  
mercoledì 12.30 - 14.30 lezione Aula I  

Obiettivi formativi

L'insegnamento presenta problemi e metodi per l'analisi e la verifica di programmi, mediante 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

Teorie al primo ordine. Induzione. 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).

Testi di riferimento
Autore Titolo Casa editrice Anno ISBN Note
Aaron R. Bradley, Zohar Manna The Calculus of Computation - Decision Procedures with Applications to Verification (Edizione 1) Springer 2007 9783540741 Testo adottato

Modalità d'esame

Per gli studenti di CdLM/LS:
Esame mediante prove parziali: 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. Questa modalità vale solo per il primo appello dopo la fine del corso.
Esame senza prove parziali: consta di un unico compito scritto (E), di difficoltà tale da uguagliare C+P, il cui voto determina il voto d'esame. Questa modalità vale per tutti gli appelli.
Per gli studenti di DdR:
esame orale consistente nella presentazione di uno o più articoli dalla letteratura.

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 90.90% 27 3
Respinti --
Assenti 4.54%
Ritirati 4.54%
Annullati --
Distribuzione degli esiti positivi
18 19 20 21 22 23 24 25 26 27 28 29 30 30 e Lode
0.0% 5.0% 0.0% 5.0% 5.0% 0.0% 0.0% 5.0% 20.0% 20.0% 0.0% 20.0% 5.0% 15.0%

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