Corso di Laurea Magistrale in Informatica

Analisi e Verifica mediante Interpretazione Astratta 2014/2015

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 – 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

• G. Winskel. The Formal Semantics of Programming Languages , The MIT Press, 1993, ISBN: 978-0-262-73103-4.
• K. R. Apt and E. Olderog. Verification of Sequential and Concurrent Programs. 2nd ed. Springer, 1997, ISBN: 0-387-94896-1.
• N.D. Jones, 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.
• 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.