Programma per l'a.a. 2000/01
Il corso ha durata di 40 ore, di cui 30 a cura del docente e
10 a cura di specialisti aziendali che illustreranno le loro
tecniche di verifica.
L'esame consiste in un colloquio individuale su
casi di studio da concordare col docente.
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
fondate da miei colleghi e che usano le tecniche che saranno presentate
nel corso:
INTRODUZIONE.
La qualità del sw, verifica di correttezza, tecniche utilizzate.
Note per scaricare i files: Con Netscape ci sono problemi, invece con
Explorer sembra che tutto vada bene. Con Netscape, posizionarsi sull'iperlink
e con il bottone di destra del mouse scegliere "Save Link As" in modo da
scaricarsi il file.
PARTE I. I sistemi dei tipi. Un caso di studio: verifica della
sicurezza in un semplice linguaggio imperativo,
semantica statica e dinamica, subject reduction.
Tipi1.pdf;
Tipi2.pdf.
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.
PARTE II. L'interpretazione astratta. Domini astratti, chiusure,
widening, narrowing, analisi degli intervalli, propagazione delle
costanti.
IntAbs1.pdf;
IntAbs2.pdf.
Riferimento: N. D. Jones, F. Nielson:
``Abstract interpretation, a semantic based tool for program analysis'',
1994
PARTE III. Proof-Carrying Code. Esecuzioni sicure di codice
insicuro, prove di safety, validatori di prove, metodi automatici per
generare le prove.
Parte3.1.pdf.
Riferimento: G. Necula:
``Proof Carrying Code'', in POPL'97, Parigi 1997.
PARTE IV. Tecniche aziendali di verifica e problemi legali
della qualità del sw.
Bibliografia. Dispense del docente e articoli reperibili sulla rete.