Verifica automatica di sistemi (2014/2015)

Codice insegnamento
4S003252
Docente
Maria Paola Bonacina
Coordinatore
Maria Paola Bonacina
crediti
6
Settore disciplinare
INF/01 - INFORMATICA
Lingua di erogazione
Italiano
Periodo
II sem. dal 2-mar-2015 al 12-giu-2015.

Orario lezioni

II sem.
Giorno Ora Tipo Luogo Note
lunedì 14.30 - 17.30 lezione Aula I  
mercoledì 16.30 - 18.30 lezione Aula I  

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.

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 100.0% 28 2
Respinti --
Assenti --
Ritirati --
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% 33.3% 0.0% 0.0% 0.0% 0.0% 0.0% 33.3% 33.3%

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