- Docente: Cosimo Laneve
- Crediti formativi: 12
- SSD: INF/01
- Lingua di insegnamento: Italiano
- Modalità didattica: Convenzionale - Lezioni in presenza
- Campus: Bologna
- Corso: Laurea Magistrale in Informatica (cod. 8028)
Conoscenze e abilità da conseguire
Al termine del corso, lo studente: - conosce le principali tecniche di analisi ed ottimizzazione del codice utilizzate nei compilatori; - conosce le tecniche di analisi statica dei programmi basate sulla interpretazione astratta; - sa analizzare il flusso dei dati in un programma; - è in grado di realizzare verificatori di semplici proprietà dei programmi; - sa dare una valutazione critica circa la tecnica da usare per garantire determinate proprietà in un programma; - è capace di elaborare e di presentare un progetto per garantire proprietà di programmi.
Contenuti
- Introduzione: le tecniche per l'analisi di programmi.
- La logica di Hoare: caso di studio su un semplice linguaggio imperativo.
- L'interpretazione astratta: domini astratti, chiusure, widening, narrowing, analisi degli intervalli, propagazione delle costanti.
- Data-flow analysis.
- Tecniche aziendali di verifica del sw.
Testi/Bibliografia
- K. Apt: Ten years of Hoare Logic: a survey", ACM Transactions on Programming Languages and Systems (TOPLAS), Volume 3 , Issue 4 (October 1981), Pages: 431 - 483.
-
D. Volpano, G. Smith, C. Irvine: ``A sound type system for secure
flow analysis'', Journal of Computer Security 1996.
-
D. Volpano, G. Smith: ``A type-based approach to program
security'', TAPSOFT'97.
- N. D. Jones, F. Nielson: ``Abstract interpretation, a semantic based tool for program analysis'', 1994
Metodi didattici
lezioni frontali.
Modalità di verifica e valutazione dell'apprendimento
esame scritto o orale.
Strumenti a supporto della didattica
proiettore.
Link ad altre eventuali informazioni
http://www.cs.unibo.it/~laneve/programanalysis
Orario di ricevimento
Consulta il sito web di Cosimo Laneve