Corsi di Laurea Corsi di Laurea Magistrale Corsi di Laurea Magistrale
a Ciclo Unico
Scuola di Scienze
INFORMATICA
Insegnamento
ANALISI STATICA E VERIFICA DEL SOFTWARE
SCM0015974, A.A. 2015/16

Informazioni valide per gli studenti immatricolati nell'A.A. 2015/16

Principali informazioni sull'insegnamento
Corso di studio Corso di laurea magistrale in
INFORMATICA
SC1176, ordinamento 2014/15, A.A. 2015/16
N0
porta questa
pagina con te
Crediti formativi 8.0
Tipo di valutazione Voto
Denominazione inglese STATIC ANALYSIS AND SOFTWARE VERIFICATION
Sito della struttura didattica http://informatica.scienze.unipd.it/2015/laurea_magistrale
Dipartimento di riferimento Dipartimento di Matematica
Obbligo di frequenza No
Lingua di erogazione INGLESE
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 8.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 8.0 64 136.0

Calendario
Inizio attività didattiche 01/10/2015
Fine attività didattiche 28/01/2016
Visualizza il calendario delle lezioni Lezioni 2019/20 Ord.2014

Commissioni d'esame
Commissione Dal Al Membri
5 a.a. 2017/2018 01/10/2017 28/02/2019 RANZATO FRANCESCO (Presidente)
BALDAN PAOLO (Membro Effettivo)
FILE' GILBERTO (Membro Effettivo)

Syllabus
Prerequisiti: Conoscenze di base dei linguaggi di programmazione. L'insegnamento non prevede propedeuticita.
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, tipicamente suddiviso in tre parti distinte.
Criteri di valutazione: L'esame orale verte su vari esercizi che lo studente deve svolgere in modo indipendente a casa.
Contenuti: - Semantica operazionale di programmi: Modellazione del comportamento operazionale dei programmi su una macchina di esecuzione mediante sistemi di regole di derivazione.

- Semantica denotazionale di programmi: Modellazione del comportamento input/output dei programmi mediante la teoria degli ordini parziali e dei punti fissi.

- Analisi statica di programmi mediante interpretazione astratta: L'interpretazione astratta è una notoria tecnica basata su una approssimazione della semantica denotazionale dei programmi che permette di specificare le proprietà dei programmi deducibili mediante analisi statica e di provarne la correttezza.

- 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 per ottimizzare un programma.

- Verifica di sistemi software mediante model checking: Il model checking e` una tecnica per la verifica automatica di proprietà di correttezza di un sistema software, dove la correttezza è specificata mediante logiche temporali. Gli inventori del model checking sono stati premiati con il prestigioso Turing Award (noto come il "Premio Nobel" dell'informatica) nel 2007.
Attivita' di apprendimento previste e metodologie di insegnamento: L'insegnamento prevede lezioni frontali e la risoluzione in modo indipendente a casa di vari esercizi.
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