Corso di Laurea Specialistica in Informatica
Tecniche Formali per l'Ingegneria del Software 2004/2005
Analisi, Debugging, Verifica e Trasformazione Automatica di Programmi basata sulla semantica
pagina aggiornata il
26-07-2005
Indice
Finalità del corso
Programma
Bibliografia
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 che stanno alla base dell'analisi automatica del software e della
verifica formale (nonchè debugging) assistiti dal calcolatore.
Prerequisiti (deboli)
Semantica dei linguaggi di Programmazione, Nozioni base su Linguaggi
Dichiarativi (Logici, Funzionali e Logico-Funzionali)
(condizione sufficiente sono i corsi di Linguaggi 1 e 2)
Programma preliminare
- Introduzione alle tecniche di trattamento del software basate sulla
semantica
- Richiami di Semantica
- Posets, CPO, Reticoli
- Semantica Operazionale
- Semantica Denotazionale
- Semantica di 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
- Verification of Sequential and Concurrent Programs. Apt, K. R. and
Olderog, E. 2nd ed., 1997, ISBN: 0-387-94896-1
- N.D. Jones and C.K. Gomard and P. Sestoft. Partial Evaluation and
Automatic Program Generation. Prentice-Hall, Englewood Cliffs, NJ,
1993.
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.
- 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.