| Nome del Corso |
Analisi di Programmi
|
| Codice del Corso |
28789
|
| Grado |
Laurea Magistrale
|
| Semestre |
Primo Semestre
|
| Docente |
Prof. Cosimo Laneve
|
| Linguaggio di Insegnamento |
Italiano
|
| Crediti |
6 cfu
|
| Ore di Insegnamento |
50
|
| 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 un caso di studio che verrà presentato a lezione e su cui sarà fatta l'attività progettuale.
|
| Syllabus |
Durante il corso si individua una proprietà che i programmi di un certo linguaggio devono verificare e si costruisce un analizzatore che prende in input un qualunque programma e stabilisce se la proprietà è verificata o meno.
Possibili linguaggi di programmazione che si considerano (cambiano di anno in anno) sono Java, Python, C#.
Possibili proprietà sono assenza di deadlock, assenza di memory leaks,
terminazione (anche esse cambiano di anno in anno). Durante il corso si studierà
la teoria da usare e si inizierà lo sviluppo dell'analizzatore da completare
come esame finale.
|
| Tipo di insegnamento |
Lezioni frontali e laboratorio
|
| Giudizio |
Progetto di gruppo.
|
| Testi di riferimento |
Di seguito una lista di possibili riferimenti. Di anno in anno saranno integrati/rimpiazzati da
altri.
[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] Molti altri: search semantics + programming languages
+ book with google and you will find tons of material.
Choose your favorite one.
|
| 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
|
| Contenuti vecchio corso |
fino all'aa 2013/14
|
|
