Automatic System Analysis and Verification (2004/2005)

Course partially running

Course code
4S00051
Name of lecturer
Roberto Giacobazzi
Number of ECTS credits allocated
5
Other available courses
Academic sector
INF/01 - INFORMATICS
Language of instruction
Italian
Period
Second four-month term dal Jan 10, 2005 al Mar 11, 2005.
Web page
http://profs.sci.univr.it/~giaco/mf.html

Lesson timetable

Second four-month term
Day Time Type Place Note
Monday 2:30 PM - 4:30 PM lesson Lecture Hall C  
Wednesday 2:30 PM - 5:30 PM lesson Lecture Hall D  

Learning outcomes

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.

Syllabus

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

Assessment methods and criteria

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.

Teaching aids

Documents