Fondamenti di analisi e verifica del software (2020/2021)

Codice insegnamento
4S008901
Docente
Isabella Mastroeni
Coordinatore
Isabella Mastroeni
crediti
6
Settore disciplinare
ING-INF/05 - SISTEMI DI ELABORAZIONE DELLE INFORMAZIONI
Lingua di erogazione
Italiano
Sede
VERONA
Periodo
I semestre dal 1-ott-2020 al 29-gen-2021.

Orario lezioni

Vai all'orario delle lezioni

Obiettivi formativi

Obiettivo del corso è quello di fornire gli strumenti base per la comprensione, la progettazione e l'utilizzo di strumenti di analisi di sistemi informatici al fine di verificare proprietà e/o estrarre funzionalità dei sistemi sotto analisi. Nel contesto del CdS, il corso fornisce quindi conoscenze di contesto e competenze di base al fine di analizzare sistemi software sia dal punto di vista di chi deve certificare proprietà desiderabili (in fase di sviluppo) che dal punto di vista di chi deve comprendere le funzionalità di un software sconosciuto (reverse engineering). Al termine dell’insegnamento lo studente dovrà essere in grado di dimostrare conoscenze e capacità di comprensione che consentono di elaborare e/o applicare idee originali nell’ambito dell’analisi e verifica di programmi, anche in contesti di ricerca; risolvere problemi di analisi e verifica di programmi in ambiti nuovi o non familiari, inseriti in contesti più ampi (o interdisciplinari) connessi al loro settore di studio; approfondire e ricercare materiale di studio riguardante temi avanzati di analisi e verifica di programmi in un modo auto-gestito o autonomo.

Programma

Introduzione all'analisi e alla verifica di programmi.
Analisi statica: Data-flow analisi su CFG, Analisi statica basata sulla semantica (Interpretazione astratta), analisi numeriche, analisi di alias e inter-procedurali (cenni).
Analisi dinamiche: Basi formali del testing, Monitoring.
Verifica: Model checking
Slicing: Tecnica di trasformazione di programmi per l'analisi e la verifica.

Testi di riferimento
Autore Titolo Casa editrice Anno ISBN Note
Seidl, Helmut, Wilhelm, Reinhard, Hack, Sebastian Compiler Design Analysis and Transformation (Edizione 1) Springer 2012 978-3-642-17548-0
Keith Cooper, Linda Torczon Engineering a Compiler, Second Edition (Edizione 2) Elsevier 2012 012088478X
Xavier Rival, Kwangkeun Yi Introduction to Static Analysis: An Abstract Interpretation Perspective MIT 2020
Edmund M Clarke, Orna Grumberg, Doron Peled, Doron Peleg Model Checking (Edizione 2) MIT 2018 9780262038836
Christel Baier and Joost-Pieter Katoen Principles of Model Checking MIT press 2008
F. Nielson, H. R. Nielson and C. Hankin Principles of Program Analysis Springer-Verlag 1999

Modalità d'esame

L'esame sarà strutturato in due parti e può essere espletato in due modi:
- Scritto + Progetto su argomenti di analisi
- Scritto + Orale (obbligatorio sopra il 26)

L'esame scritto ha l'obiettivo di verificare una sufficiente acquisizione e comprensione dei concetti presentati nel corso.
Il progetto ha l'obiettivo di verificare la capacità di acquisire materiale di studio e di rielaborare autonomamente i concetti presentati durante il corso.
L'esame orale ha l'obiettivo di verificare una acquisizione ed una comprensione avanzata dei concetti studiati, con capacità di rielaborazione degli stessi.

In particolare:
Scritto: Insieme domande per valutare la preparazione dello studente sull'intero programma del corso.
- Progetto/approfondimento fatto da gruppi di massimo due persone il cui argomento può essere anche proposto al docente da parte del gruppo stesso. Tale progetto dovrà essere completato con una relazione scritta che verrà presentata in forma orale (con slide).
- Orale: Domande orali sull'intero programma del corso, in caso di voto superiore a 26/30 allo scritto, l'orale diventa obbligatorio, altrimenti si può registrare massimo un 26.