| Nome del Corso |
Metodi Formali 1: Qualità del Software
|
| Codice del Corso |
30217
|
| Grado |
Laurea Magistrale
|
| Semestre |
Primo Semestre
|
| Docente |
Prof. Cosimo Laneve
|
| Linguaggio di Insegnamento |
Italiano
|
| Crediti |
6
|
| Ore di Insegnamento |
40
|
| Orario |
vai a
http://www.informatica.unibo.it/cdl/informatica/
|
| Orario di Ricevimento |
Martedì 12,00 -- 13.30
|
| Obiettivi |
Questo corso consente di apprendere le tecnologie formali
più importanti per garantire proprietà di correttezza
importanti di programmi commerciali (qualità del software). Ad esempio,
la terminazione di programmi real-time, la deadlock-freeness di programmi
concorrenti, accessi a dati condivisi con rispetto dei propri privilegi.
Tutte le tecniche presentate saranno applicate a casi di studio.
Alcune ore saranno svolte da specialisti aziendali che illustreranno casi
reali di verifica.
|
| Syllabus |
- Introduzione: la qualità del sw, verifica di correttezza, tecniche utilizzate.
- I sistemi dei tipi: verifica della sicurezza in un semplice linguaggio imperativo, semantica statica e dinamica, subject reduction.
- L'interpretazione astratta: domini astratti, chiusure, widening, narrowing, analisi degli intervalli, propagazione delle costanti.
- Proof-Carrying Code: esecuzioni sicure di codice insicuro, prove di safety, validatori di prove, metodi automatici per generare le prove.
- Tecniche aziendali di verifica e problemi legali della qualità del sw.
|
| Tipo di insegnamento |
Lezioni frontali
|
| Giudizio |
Esame orale
|
| Testi di riferimento |
- 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
- G. Necula: ``Proof Carrying Code'', in POPL'97, Parigi 1997.
|
| Captatio Benevolentiae |
Qui
trovate una buona ragione per la verifica della qualità del
software. Qui
trovate un'applicazione della verifica di qualità in cui
dimostriamo che tutti i compilatori Java hanno bachi.
Alcune start-up sulla verifica della qualità del sw
che usano le tecniche che saranno presentate nel corso:
|
| Lucidi delle Lezioni |
Introduzione.pdf; Tipi1.pdf;
Tipi2.pdf;
IntAbs1.pdf; IntAbs2.pdf;
PCC.pdf
|
| Risultati del corso |
Dopo questo corso, gli studenti comprenderanno
le tecniche formali per garantire proprietà di correttezza di
programmi, le difficoltà relative alla loro progettazione e
i possibili campi di applicazione.
|
| Newsgroup |
unibo.cs.mf1
|
|
