Introduzione:
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, ovvero a ciò che i programmi fanno indipendentemente
dalla loro rappresentazione in un dato linguaggio di
programmazione. Ad esempio, nei moderni sistemi distribuiti WWW
è spesso necessario assicurare un corretto e sicuro flusso di
informazioni affinchè non vengano violate privacy o venga
compromessa la sicurezza dei sistemi di elaborazione. Analogamente,
nei compilatori è importante conoscere il flusso delle
informazioni all'interno delle varie strutture del programma (ovvero
la semantica del programma) per potere trasformare questo al fine di
ottenere un programma semanticamente equivalente ma migliore in
prestazioni. Questi problemi sono risolti da strumenti largamente
utilizzati nei moderni browsers e compilatori per verificare ed
ottimizzare il codice importato dall'esterno o prodotto in fase di
compilazione. Tuttavia, la natura indecidibile dei problemi legati
alla semantica dei linguaggi di programmazione, 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. A partire da una semantica molto concreta
(vicina all'esecuzione reale dei programmi) di un generico linguaggio
di programmazione, verranno introdotti strumenti e tecniche per
specificare, verificare ed approssimare proprietà di programmi.
Il Corso:
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
Testi
Appunti distribuiti a lezione
H. A. Priestley, "Ordered sets and complete lattices"
PDF
Burris and Sankappanavar, "A Course in Universal Algebra."
PDF
Davey and Priestley, "Introduction to Lattices and Order",
Cambridge, 1992
J.B. Nation, "Notes on Lattice Theory."
PDF
Nielson, Nielson and Hankin, "Principles of Program Analysis",
Springer-Verlag, 1999
Winskel, "The formal Semantics of Programming Languages"
MIT Press, 1993
F. Nielson and H.R. Nielson, "
Semantics
with Applications" accessibile via web.
Clarke, Grumberg and Peled, "Model Checking", MIT Press, 2000
I. Mastroeni, "Model checking astratto"
PS
Cousot and Cousot, "Abstract Interpretation of Logic Programs."
PS