Corso di Laurea Magistrale in Informatica
Analisi e Verifica mediante Interpretazione Astratta 2016/2017
Analisi, Debugging, Verifica e Trasformazione Automatica di Programmi basata sulla semantica (astratta)
pagina aggiornata il
23-09-2016
VERSIONE PRELIMINARE
Indice
Finalità del corso
La crescente dipendenza della società dalle applicazioni
informatiche fa sí che l'analisi e la verifica della correttezza dei
sistemi complessi rappresenti sempre di più un fattore critico del
processo di sviluppo. Il malfunzionamento dei sistemi, siano essi hardware,
software o protocolli di comunicazione, può comportare danni
rilevanti di ogni genere: dalla perdita finanziaria alla perdita di vite
umane. Inoltre, quando i difetti non sono rilevati prima dell'impiego del
sistema, l'applicazione di eventuali misure correttive è, quando
possibile, ben più difficile e costosa. Esempi dal recente passato
includono il millennium bug, gli errori di alcune versioni del processore
Pentium, lo scoperto da 32 miliardi di dollari alla N.Y. Bank, il
fallimento iniziale del vettore Ariane 5, e gli incidenti mortali del
Therac-25.
Il corso intende fornire una introduzione (relativamente) estesa alle
tecniche – basate sull'interpretazione astratta – che stanno alla base dell'analisi
automatica del software e della verifica formale (nonchè debugging)
assistiti dal calcolatore.
Prerequisiti
- Nozioni base su Linguaggi
Imperativi e Dichiarativi (grammatiche, sintassi astratta)
Programma preliminare
- Introduzione alle tecniche di trattamento del software basate sulla
semantica
- Posets, CPO, Reticoli
- Semantica mediante Punto Fisso
- Da programmi a proprietà: Analisi statica
di programmi
-
Schemi monotoni: Esempi di DFA (Data-flow analysis)
- Interpretazione astratta.
- Ottimizzazione di un programma imperativo;
- reticoli completi econnessioni di Galois
- upper closure operators;
- Semantiche standard e non standard della programmazione
logica;
- Domini astratti per l'ottimizzazione della programmazione
dichiarativa: Pos, Def e Sharing;
- Disegno di domini astratti: prodotto ridotto,
complementazione, raffinamenti e loro inversione;
- Tecniche di accelerazione del punto fisso
(Widening/Narrowing)
- Applicazioni
- Da programmi a programmi: Trasformazione e
Valutazione parziale
- trasformazione
- ottimizzazione mediante partial evaluation
- Con programmi e proprietà: Debugging e
Verifica
- Specifiche e proprietà di programmi.
- Debugging Algoritmico
- Abstract Diagnosis
- Logica di Hoare e verifica di programmi sequenziali.
- Asserzioni come dominio astratto
- Abstract Verification: Analisi e verifica, verso una teoria
unificante.
- Type checking come caso particolare di Abstract
Verification
- Da proprietà a programmi: Sintesi di
Programmi
Bibliografia
Libri
Articoli (e materiale di riferimento reperibile in rete)
- Articolo di Cousot con un'esauriente illustrazione
dell'interpretazione astratta: Patrick Cousot & Radhia
Cousot.
Abstract
interpretation and application to logic programs. Journal of Logic
Programming, 13(2–3):103–179, 1992
- La mia Tesi di Dottorato: M. Comini.
An
abstract interpretation framework for Semantics and Diagnosis of logic
programs. Ph.D. thesis TD-5/98, Dipartimento di
Informatica, Università di Pisa, 1998.
- M. Comini, R. Gori, G. Levi, P. Volpe.
Abstract
Interpretation based Verification of Logic Programs. Science of
Computer Programming, 49(1–3):89–123, 2003.
- A. Cortesi, G. Filé.
Sharing
is optimal. Journal of Logic Programming, 38(3):371–386, 1999
- A. Cortesi, G. Filé, W. Winsborough.
Optimal
groundness analysis using propositional logic. Journal of Logic Programming,
27(2):137–167, 1996
- R. Giacobazzi, F. Ranzato:
Completeness
in Abstract Interpretation: A Domain Perspective. AMAST 1997: 231-245
- A. Pettorossi, M. Proietti.
MAP:
A Tool for Program Transformation.
- P. Cousot.
Semantic
foundations of program analysis. In S.S. Muchnick and N.D. Jones,
editors, Program Flow Analysis: Theory and Applications, chapter
10, pages 303—342. Prentice-Hall, Inc., Englewood Cliffs, New
Jersey, USA, 1981.
- P. Cousot.
Abstract
interpretation based formal methods and future challenges, invited
paper. In R. Wilhelm, editor, « Informatics — 10
Years Back, 10 Years Ahead », volume 2000 of Lecture
Notes in Computer Science, pages 138–156. Springer-Verlag, 2000.
- R. Giacobazzi, F. Ranzato, F. Scozzari.
Making
Abstract Domains Condensing.
ACM Transactions on Computational Logic (TOCL). 6(1):33–60, 2005.
- R. Giacobazzi, F. Ranzato, F. Scozzari.
Making
abstract interpretations complete. Journal of the ACM. 47(2):361–416,
2000.
- R. Giacobazzi, F. Scozzari.
A
logical model for relational abstract domains. ACM Transactions on
Programming Languages and Systems 20(5):1067–1109, 1998.
- P. Cousot, R. Cousot.
Comparing
the Galois connection and widening/narrowing approaches to abstract interpretation.
In M. Bruynooghe & M.
Wirsing, editors, Programming Language Implementation and Logic Programming,
PLILP'92, Lecture Notes in
Computer Science 631, pages 269—295. Springer, 1992.
- P. Cousot, R. Cousot.
Higher-order
abstract interpretation (and application to comportment analysis generalizing
strictness, termination, projection and PER analysis of functional languages).
In Proceedings of ICCL'94, pages 95—112. IEEE
Computer Society Press, 1994.