Cosimo Laneve's home page @ unibo

Department of Computer Science and Engineering

Corso di Analisi di Programmi

Nome del Corso	Analisi di Programmi
Codice del Corso	28789
Grado	Laurea Magistrale
Semestre	Primo e Secondo Semestre
Docente	Prof. Cosimo Laneve
Linguaggio di Insegnamento	Italiano
Crediti	6 cfu (fino all'a.a. 2010/11: 12cfu)
Ore di Insegnamento	40 (fino all'a.a. 2010/11: 80)
Orario	vai a http://corsi.unibo.it/informatica-magistrale
Orario di Ricevimento	Su appuntamento via email (di solito il Mercoledì 12,00 -- 13.30
Obiettivi	Questo corso consente di apprendere le tecnologie formali più importanti per garantire proprietà di correttezza di programmi commerciali o presenti nei compilatori per ottimizzare i codici. Tutte le tecniche presentate saranno applicate a casi di studio.
Syllabus a.a. 2011/12	Lecture 1. Introduzione, nozioni preliminari (insiemi, prodotti cartesian i, relazioni, funzioni, funzioni parzialie totali, spazi di funzioni, concatenzazione di funzioni), il linguaggio whil e: sintassi. [1], pg. 213-214, 7-9. Lecture 2.Semantica denotazionale del linguaggio while: semantica delle espressioni intere e semantica delle espressioni booleane. [1], pg 9-17. Lecture 3. Semantica denotazionale del linguaggio while: la semantica dei comandi, criteri per le equazioni di punto fisso. [1], pg 85-89. Lecture 4: Teoria del punto fisso: ordinamenti parziali, ordinamenti parziali completi, reticoli, funzioni monotone, funzioni continue, il teorema di Kleene. [1], pg 93-107; [2], pg 393-404. Lecture 5. La semantica del comando while e di altri comandi iterativi. [1], pg 107-112. Lecture 6: Data-Flow Analysis: analisi delle available espressions, [2], pg. 35-43. Lecture 7: Data Flow Analysis: analisi delle definizioni raggiungibili e constant folding, [2], pg. 43-46, 27-29. Lecture 8: Data Flow Analysis: analisi delle very busy espressions, [2], pg 46-49. Lecture 9: Data-Flow Analysis: analisi delle variabili vive, [2], pg. 49-52. Lecture 10: Data Flow Analysis: correttezza dell'analisi delle variabili vive, [2], pg. 60-65. Lecture 11: Data-Flow Analysis: le equazioni di dataflow, loro soluzione algoritmica e complessità computazionale, [2], pg. 65-82, 365-392. Lecture 12: Data-Flow Analysis: problemi non distributivi, l'analisi della propagazione delle costanti, e l'algoritmo relativo, [2], pg. 72-74 e 78-82. Lecture 13: Interpretazione Astratta: domini astratti e domini concreti, connessioni di Galois e inserzioni di Galois. Il dominio astratto dei segni. [6] Lecture 14: Interpretazione Astratta: la semantica astratta delle espressioni (del linguaggio while) e la correttezza locale delle operazioni. [6]
Syllabus fino all'a.a. 2010/11	Lecture 1. Introduzione, nozioni preliminari (insiemi, prodotti cartesiani, relazioni, funzioni, funzioni parziali e totali, spazi di funzioni, concatenzazione di funzioni), il linguaggio while: sintassi. [1], pg. 213-214, 7-9. Lecture 2. Semantica denotazionale del linguaggio while: semantica delle espressioni intere e semantica delle espressioni booleane. [1], pg 9-17. Lecture 3. Semantica denotazionale del linguaggio while: la semantica dei comandi, criteri per le equazioni di punto fisso. [1], pg 85-89. Lecture 4: Teoria del punto fisso: ordinamenti parziali, ordinamenti parziali completi, reticoli, funzioni monotone, funzioni continue, il teorema di Kleene. [1], pg 93-107; [2], pg 393-404. Lecture 5. La semantica del comando while e di altri comandi iterativi. [1], pg 107-112. Lecture 6: La logica di Hoare: correttezza parziale, esempio di verifica con la semantica denotazionale, variabili logiche, il linguaggio delle asserzioni. [1], pg 172-177. Lecture 7: La logica di Hoare: le regole, invarianti, proprieta`. [1], pg 178-183. Lecture 8: La logica di Hoare: consistenza e completezza del sistema. [1], pg 183-191. Lecture 9: Data-Flow Analysis: analisi delle available espressions, [2], pg. 35-43. Lecture 10: Data Flow Analysis: analisi delle definizioni raggiungibili e constant folding, [2], pg. 43-46, 27-29. Lecture 11: Data Flow Analysis: analisi delle very busy espressions, [2], pg 46-49. Lecture 12: Data-Flow Analysis: analisi delle variabili vive, [2], pg. 49-52. Lecture 13: Data Flow Analysis: correttezza dell'analisi delle variabili vive, [2], pg. 60-65. Lecture 14: Data-Flow Analysis: le equazioni di dataflow, loro soluzione algoritmica e complessità computazionale, [2], pg. 65-82, 365-392. Lecture 15: Data-Flow Analysis: problemi non distributivi, l'analisi della propagazione delle costanti, e l'algoritmo relativo, [2], pg. 72-74 e 78-82. Lecture 16: Interpretazione Astratta: domini astratti e domini concreti, connessioni di Galois e inserzioni di Galois. Il dominio astratto dei segni. [6] Lecture 17: Interpretazione Astratta: la semantica astratta delle espressioni (del linguaggio while) e la correttezza locale delle operazioni. [6] Lecture 18: Interpretazione Astratta: la semantica astratta dei comandi del linguaggio while. [6] Lecture 19: Interpretazione Astratta: la correttezza della semantica astratta del linguaggio while. [6] Lecture 20: Interpretazione Astratta: Caso di studio: il Java Bytecode Verifier (1). [6] Lecture 21: Interpretazione Astratta: Caso di studio: il Java Bytecode Verifier (2). [6] Lecture 22: Interpretazione Astratta: Caso di studio: il Java Bytecode Verifier (3). [6]
Tipo di insegnamento	Lezioni frontali
Giudizio	Esame scritto
Testi di riferimento	[1] Hanne Riis Nielson, Flemming Nielson: Semantics with Applications: A Formal Introduction. [2] F. Nielson, H.R. Nielson, C. Hankin: "Principles of Program Analysis", Springer Verlag, 2005 [3] K. R. Apt: "Ten years of Hoare logic: A survey -- Part 1", ACM Transactions on Programmming Languages, Vol. 3(4), pp. 431--483, 1981. [4] N. D. Jones, F. Nielson: "Abstract interpretation, a semantic based tool for program analysis", 1994 [5] Glynn Winskel: Lecture notes on Denotational semantics. [6] Dispense del docente: Parte 0 Parte 1, Parte 2, Parte 3. [7] B. A. Davey, H. A. Priestley: Introduction to Lattices and Order. This is the Bible for cpos, lattices, etc. For outstanding students only. [8] many others: search semantics + programming languages + book with google and you will find tons of material. Choose your favorite one.
Captatio Benevolentiae	Qui si trovano buone ragioni per studiare l'analisi dei programmi. Qui si trova un'applicazione dell'analisi dei programmi in cui si dimostria che tutti i compilatori Java -- SDK 1.3 hanno bachi (il problema e` stato risolto dall'SDK 1.4 in poi). Alcune start-up che usano le tecniche che saranno presentate nel corso: Polyspace Trusted Logic
Risultati del corso	Comprensione di tecniche formali per garantire proprietà di correttezza di programmi, le difficoltà relative alla loro progettazione e i possibili campi di applicazione.
Newsgroup	unibo.cs.informaticamagistrale.analisidiprogrammi