ANALISI E VERIFICA DI PROGRAMMI

AA 2009/'10

prof. A. Cortesi

Risultati dei questionari di Valutazione degli studenti

Obiettivo

L'obiettivo del corso e` fornire una conoscenza sull'applicazione di metodi formali per l'analisi e la verifica di programmi.

Programma

• Panoramica dei metodi formali di analisi e verifica di programmi: caratteristiche e limiti
• Ordini Parziali e Reticoli
• Punti Fissi e operatori di widening
• Semantiche astratte
• Interpretazione astratta
• Analisi statica basata su analisi dataflow
• Analisi classiche di liveness, reaching definition, constant propagation, etc.
• Trasformazioni e ottimizzazioni del codice basate sull'analisi
• Model Checking di sistemi a stati finiti: specifica del sistema e delle proprieta' da verificare, logiche temporali.
• Casi di studio e temi avanzati di ricerca
• Esercitazioni in laboratorio

Testi di riferimento

• F.Nielson, H.R.Nielson, C. Hankin: Principles of Program Analysis, Springer Verlag, 2004
• B.Berard et al., Systems and Software Verifications. Springer Verlag 2001.

Materiale Corso di Laboratorio

• The Java Virtual Machine Specification (HTML, in particolare capitolo 6 HTML)
• jclasslib (Freeware), programma per vedere il bytecode contenuto in un file .class

Modalita' d'esame

Discussione di un progetto (da svolgersi a coppie) e prova orale sul contenuto del corso.

Progetto AA 2009/10:

• IMPORTANTE: Inviate subito una mail a pietro.ferrara@gmail.com per poter ricevere ulteriori comunicazioni sul progetto.
• Slides su Domini Non Relazionali
• Slides su Domini Relazionali
• Slides su Heap Analysis
• Descrizione Progetto 2009
• Tutto il materiale utile alla realizzazione del progetto