Corso di Laurea Specialistica in Informatica

Interpretazione Astratta e Analisi Automatica del Software 2007/2008

Analisi, Debugging, Verifica e Trasformazione Automatica di Programmi basata sulla semantica

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 che stanno alla base dell'analisi automatica del software e della verifica formale (nonchè debugging) assistiti dal calcolatore.

Prerequisiti

• Semantica dei linguaggi di Programmazione
  (condizione sufficiente è il corso di 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.