Analisi e verifica automatica di sistemi (2004/2005)

Corso a esaurimento

Codice insegnamento
4S00051
Docente
Roberto Giacobazzi
crediti
5
Altri corsi di studio in cui è offerto
Settore disciplinare
INF/01 - INFORMATICA
Lingua di erogazione
Italiano
Periodo
2° Q dal 10-gen-2005 al 11-mar-2005.
Pagina Web
http://profs.sci.univr.it/~giaco/mf.html

Orario lezioni

2° Q
Giorno Ora Tipo Luogo Note
lunedì 14.30 - 16.30 lezione Aula C  
mercoledì 14.30 - 17.30 lezione Aula D  

Obiettivi formativi

Un aspetto fondamentale della moderna scienza dei calcolatori è quello
di fornire strumenti per poter ragionare sulle proprietà dei programmi.
Le proprietà più interessanti sono quelle legate alla semantica dei
programmi. La natura
indecidibile di questi problemi, impone una necessaria approssimazione
nella fase di analisi e verifica formale. Nel corso vengono studiati i principali
metodi formali per costruire sistematicamente strumenti per l'analisi
statica e la verifica automatica di proprietà di programmi scritti in un
linguaggio di programmazione (qualunque esso sia) mediante tecniche di
approssimazione semantica. Verranno introdotti strumenti e tecniche per
specificare, verificare ed approssimare proprietà significative di
componenti Software complessi.

Programma

Programma
# Introduzione all'analisi e verifica di sistemi complessi
# Posets, CPO, Reticoli, e Teoremi di punto fisso
# Specifiche e proprietà di programmi
# Logica di Hoare e verifica di programmi sequenziali
# Sistemi reattivi e concorrenti
# Logiche temporali: CTL*, CTL, LTL
# Model Checking
# Symbolic model checking
# Astrazione e connessioni di Galois
# Correttezza e astrazione di sistemi
# Approssimazione semantica: Interpretazione astratta
# Analisi statica e verifica: verso una teoria unificante

Modalità d'esame

Orale con discussione di una tesina (applicata o teorica) su un argomento dato dal docente. L'esame prevede anche la valutazione di homeworks dati dal docente durante le lezioni.

Materiale didattico

Documenti

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% 30 0
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% 0.0% 0.0% 0.0% 0.0% 0.0% 0.0% 16.6% 83.3%

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