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,
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.
Attività formative
Il corso prevede una attività di laboratorio (circa 10h) ad
integrazione della parte teorica. Scopo della parte di laboratorio
è quella di familiarizzare con strumenti di analisi
automatica del SW e di fornire le basi per la progettazione di
semplici analizzatori statici e strumenti di verifica automatica di
programmi.
Programma del corso
- 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
- Analisi statica di programmi
- Schemi monotoni: Esempi di DFA (Data-flow analysis)
- Approssimazione semantica: Interpretazione astratta
- Tecniche di accelerazione del punto fisso
(Widening/Narrowing)
- Analisi e verifica: verso una teoria unificante
TESTI
- Appunti distribuiti a lezione
- Davey and Priestley, "Introduction to Lattices and
Order", Cambridge, 1992
- Nielson, Nielson and Hankin, "Principles of Program
Analysis", Springer-Verlag, 1999
- Winskel, "The formal Semantics of Programming Languages"
MIT Press, 1993
- Clarke, Grumberg and Peled, "Model Checking", MIT Press,
2000