ANALYSIS AND VERIFICATION OF SOFTWARE
[English] AF: 153929 AR: 66123
| Titolo corso in inglese | ANALYSIS AND VERIFICATION OF SOFTWARE |
| Anno Accademico | 2012/2013 |
| Codice Insegnamento | CM0230 |
| Crediti formativi universitari | 6 |
| Livello laurea | Laurea Magistrale dm270 |
| Settore scientifico disciplinare | INF/01 |
| Periodo | II Semestre |
| Anno corso | 1 |
| Sede | VENEZIA |
Docenti
Corsi di laurea e percorsi
Orario settimanale
| Giorno | Ora | Sede | Aula |
|---|
| Lunedì | 08:45 - 10:15 | Polo scientifico via Torino | AULA B |
| Data | Attività | Note |
|---|---|---|
| 04/02/2013 | Lezione | CORTESI Agostino |
| 11/02/2013 | Lezione | CORTESI Agostino |
| 18/02/2013 | Lezione | CORTESI Agostino |
| 25/02/2013 | Lezione | CORTESI Agostino |
| 04/03/2013 | Lezione | CORTESI Agostino |
| 11/03/2013 | Lezione | CORTESI Agostino |
| 18/03/2013 | Lezione | CORTESI Agostino |
| 25/03/2013 | Lezione | CORTESI Agostino |
| 15/04/2013 | Lezione | CORTESI Agostino |
| 22/04/2013 | Lezione | CORTESI Agostino |
| 29/04/2013 | Lezione | CORTESI Agostino |
| Lunedì | 10:30 - 12:00 | Polo scientifico via Torino | AULA B |
| Data | Attività | Note |
|---|---|---|
| 08/04/2013 | Lezione | CORTESI Agostino |
| Venerdì | 08:45 - 10:15 | Polo scientifico via Torino | AULA B |
| Data | Attività | Note |
|---|---|---|
| 08/02/2013 | Lezione | CORTESI Agostino |
| 15/02/2013 | Lezione | CORTESI Agostino |
| 22/02/2013 | Lezione | CORTESI Agostino |
| 01/03/2013 | Lezione | CORTESI Agostino |
| 08/03/2013 | Lezione | CORTESI Agostino |
| 15/03/2013 | Lezione | CORTESI Agostino |
| 22/03/2013 | Lezione | CORTESI Agostino |
| 29/03/2013 | Lezione | CORTESI Agostino |
| 05/04/2013 | Lezione | CORTESI Agostino |
| 12/04/2013 | Lezione | CORTESI Agostino |
| 19/04/2013 | Lezione | CORTESI Agostino |
| 26/04/2013 | Lezione | CORTESI Agostino |
| 03/05/2013 | Lezione | CORTESI Agostino |
Calendario delle lezioni
| Lezione | Aula | Note |
|---|---|---|
| 04/02/2013 Lun 08:45-10:15 | Polo scientifico via Torino - AULA B | CORTESI Agostino Lezione |
| 08/02/2013 Ven 08:45-10:15 | Polo scientifico via Torino - AULA B | CORTESI Agostino Lezione |
| 11/02/2013 Lun 08:45-10:15 | Polo scientifico via Torino - AULA B | CORTESI Agostino Lezione |
| 15/02/2013 Ven 08:45-10:15 | Polo scientifico via Torino - AULA B | CORTESI Agostino Lezione |
| 18/02/2013 Lun 08:45-10:15 | Polo scientifico via Torino - AULA B | CORTESI Agostino Lezione |
| 22/02/2013 Ven 08:45-10:15 | Polo scientifico via Torino - AULA B | CORTESI Agostino Lezione |
| 25/02/2013 Lun 08:45-10:15 | Polo scientifico via Torino - AULA B | CORTESI Agostino Lezione |
| 01/03/2013 Ven 08:45-10:15 | Polo scientifico via Torino - AULA B | CORTESI Agostino Lezione |
| 04/03/2013 Lun 08:45-10:15 | Polo scientifico via Torino - AULA B | CORTESI Agostino Lezione |
| 08/03/2013 Ven 08:45-10:15 | Polo scientifico via Torino - AULA B | CORTESI Agostino Lezione |
| 11/03/2013 Lun 08:45-10:15 | Polo scientifico via Torino - AULA B | CORTESI Agostino Lezione |
| 15/03/2013 Ven 08:45-10:15 | Polo scientifico via Torino - AULA B | CORTESI Agostino Lezione |
| 18/03/2013 Lun 08:45-10:15 | Polo scientifico via Torino - AULA B | CORTESI Agostino Lezione |
| 22/03/2013 Ven 08:45-10:15 | Polo scientifico via Torino - AULA B | CORTESI Agostino Lezione |
| 25/03/2013 Lun 08:45-10:15 | Polo scientifico via Torino - AULA B | CORTESI Agostino Lezione |
| 29/03/2013 Ven 08:45-10:15 | Polo scientifico via Torino - AULA B | CORTESI Agostino Lezione |
| 05/04/2013 Ven 08:45-10:15 | Polo scientifico via Torino - AULA B | CORTESI Agostino Lezione |
| 08/04/2013 Lun 10:30-12:00 | Polo scientifico via Torino - AULA B | CORTESI Agostino Lezione |
| 12/04/2013 Ven 08:45-10:15 | Polo scientifico via Torino - AULA B | CORTESI Agostino Lezione |
| 15/04/2013 Lun 08:45-10:15 | Polo scientifico via Torino - AULA B | CORTESI Agostino Lezione |
| 19/04/2013 Ven 08:45-10:15 | Polo scientifico via Torino - AULA B | CORTESI Agostino Lezione |
| 22/04/2013 Lun 08:45-10:15 | Polo scientifico via Torino - AULA B | CORTESI Agostino Lezione |
| 26/04/2013 Ven 08:45-10:15 | Polo scientifico via Torino - AULA B | CORTESI Agostino Lezione |
| 29/04/2013 Lun 08:45-10:15 | Polo scientifico via Torino - AULA B | CORTESI Agostino Lezione |
| 03/05/2013 Ven 08:45-10:15 | Polo scientifico via Torino - AULA B | CORTESI Agostino Lezione |
Programma
Obiettivi Formativi
Lo scopo del corso e introdurre le principali tecniche di analisi statica di programmi, che permettono di derivare a tempo di compilazione approssimazioni corrette relative al comportamento dinamico di un programma. I principali campi di applicazione di queste tecniche riguardano l'ottimizzazione dei compilatori e la certificazione di programmi.
Prerequisiti
--
Contenuti
Introduzione all'analisi di programmi.
Tecniche di interpretazione astratta.
Tecniche di Data-Flow Analysis.
Tecniche di Model Checking.
Testi di riferimento
F. Nielson, H.R. Nielson, and C. Hankin: Principles of Program Analysis, Springer 2003.
Berard et al.: Systems and Software Verification, Springer 2001.
Modalità di verifica dell'apprendimento
orale
Metodi didattici
lezioni frontali e team work su un progetto di specializzazione di un analizzaatore statico
Lingua di insegnamento
inglese
Sostenibilità
- Dispense e materiali di approfondimento e di autovalutazione disponibili online; testi di riferimento in formato e-book
- Forum virtuali, blog, wikis
