Analisi e verifica automatica di sistemi (2007/2008)

Corso a esaurimento

Codice insegnamento
4S00051
Docente
Roberto Giacobazzi
crediti
5
Settore disciplinare
INF/01 - INFORMATICA
Lingua di erogazione
Italiano
Periodo
2° Q dal 10-gen-2008 al 12-mar-2008.

Orario lezioni

2° Q
Giorno Ora Tipo Luogo Note
lunedì 11.30 - 13.30 lezione Aula I  
mercoledì 10.30 - 13.30 lezione Aula G  

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, trasformare, verificare ed approssimare proprietà significative di
componenti Software complessi. In particolare verranno affrontati i problemi di sicurezza del software (information flow analysis, code obfuscation, software watermarking e malware detection).

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
# Elementi di Sicurezza del software.

Modalità d'esame

Orale con discussione di una tesina (applicata o teorica) su un argomento dato dal docente.