Corsi di Laurea Corsi di Laurea Magistrale Corsi di Laurea Magistrale
a Ciclo Unico
Scuola di Scienze
INFORMATICA
Insegnamento
VERIFICA DEL SOFTWARE
SCP6076339, A.A. 2017/18

Informazioni valide per gli studenti immatricolati nell'A.A. 2017/18

Principali informazioni sull'insegnamento
Corso di studio Corso di laurea magistrale in
INFORMATICA
SC1176, ordinamento 2014/15, A.A. 2017/18
N0
porta questa
pagina con te
Crediti formativi 6.0
Tipo di valutazione Voto
Denominazione inglese SOFTWARE VERIFICATION
Sito della struttura didattica http://informatica.scienze.unipd.it/2017/laurea_magistrale
Dipartimento di riferimento Dipartimento di Matematica
Obbligo di frequenza No
Lingua di erogazione ITALIANO
Sede PADOVA
Corso singolo È possibile iscriversi all'insegnamento come corso singolo
Corso a libera scelta È possibile utilizzare l'insegnamento come corso a libera scelta

Docenti
Responsabile FRANCESCO RANZATO INF/01

Dettaglio crediti formativi
Tipologia Ambito Disciplinare Settore Scientifico-Disciplinare Crediti
CARATTERIZZANTE Discipline Informatiche INF/01 6.0

Organizzazione dell'insegnamento
Periodo di erogazione Primo semestre
Anno di corso I Anno
Modalità di erogazione frontale

Tipo ore Crediti Ore di
didattica
assistita
Ore Studio
Individuale
LEZIONE 6.0 48 102.0

Calendario
Inizio attività didattiche 02/10/2017
Fine attività didattiche 19/01/2018

Commissioni d'esame
Commissione Dal Al Membri
3 a.a. 2018/2019 01/10/2018 28/02/2020 RANZATO FRANCESCO (Presidente)
FILE' GILBERTO (Membro Effettivo)
CRAFA SILVIA (Supplente)
GAGGI OMBRETTA (Supplente)
SPERDUTI ALESSANDRO (Supplente)

Syllabus
Prerequisiti: Conoscenze di base dei linguaggi di programmazione. L'insegnamento non prevede propedeuticità.
Conoscenze e abilita' da acquisire: Il corso mira ad introdurre metodi e strumenti per la specifica del comportamento, l'analisi statica e la verifica automatica dei programmi e, più in generale, dei sistemi software. In particolare, il corso fornisce una introduzione alla semantica formale dei linguaggi di programmazione ed ai metodi formali per la loro analisi statica e verifica.
Modalita' di esame: Esame orale e/o progetto software, possibilmente suddivisi in parti distinte.
Criteri di valutazione: L'esame orale verte su vari esercizi che lo studente deve svolgere in modo indipendente a casa. Il progetto di laboratorio verte su qualche tool di verifica del software.
Contenuti: - Semantica dei programmi: Modellazione del comportamento (in particolare il comportamento input/output) dei programmi mediante la teoria dell'ordinamento e dei punti fissi. (cf. https://en.wikipedia.org/wiki/Semantics_(computer_science) )

- Analisi statica e verifica di programmi mediante interpretazione astratta: L'interpretazione astratta è una notoria tecnica basata su una approssimazione della semantica dei programmi che permette di specificare le proprietà dei programmi deducibili mediante analisi statica e di provarne la correttezza. (cf. https://en.wikipedia.org/wiki/Abstract_interpretation )

- Analisi statica dataflow di programmi: tecnica per dedurre staticamente informazioni sull'insieme dei possibili valori delle variabili nei vari punti del programma. Un grafo di flusso del controllo è utilizzato per determinare le parti di un programma a cui un particolare valore assegnato ad una variabile potrebbe propagarsi. Le informazioni raccolte sono spesso utilizzate dai compilatori (come gcc e javac) per ottimizzare un programma. (cf. https://en.wikipedia.org/wiki/Data-flow_analysis )

- Strumenti di verifica del software: ad esempio, Clousot (Microsoft, USA), Interproc (INRIA, Francia), Jandom (Università di Pescara) (cf. https://en.wikipedia.org/wiki/List_of_tools_for_static_code_analysis )

- Il corso ospiterà dei seminari invitati tenuti dal prof. Antoine Minè della Universitè Pierre et Marie Curie di Parigi (https://www-apr.lip6.fr/~mine ) su aspetti avanzati dell'analisi statica di variabili numeriche dei programmi.
Attivita' di apprendimento previste e metodologie di insegnamento: L'insegnamento prevede lezioni frontali e la risoluzione in modo indipendente a casa di vari esercizi e/o lo sviluppo di un progetto di verifica del software.
Eventuali indicazioni sui materiali di studio: Le slide utilizzate a lezione verranno distribuite.
Testi di riferimento:
  • H. Riis Nielson, F. Nielson, Semantics with Applications: A Formal Introduction. --: Wiley, 1992. Electronic version freely available