Presentazione

Organizzazione della Didattica

DM270
INFORMATICA ORD. 2014

Analisi statica e verifica del software

8

Corsi comuni

 

Frontali Esercizi Laboratorio Studio Individuale
ORE: 64 0 0 136

Periodo

AnnoPeriodo
I anno1 semestre

Frequenza

Facoltativa

Erogazione

Convenzionale

Lingua

Inglese

Calendario Attività Didattiche

InizioFine
01/10/201424/01/2015

Tipologia

TipologiaAmbitoSSDCFU
caratterizzanteDiscipline informaticheINF/018


Responsabile Insegnamento

ResponsabileSSDStruttura
Prof. RANZATO FRANCESCOINF/01Dipartimento di Matematica

Altri Docenti

Non previsti

Attività di Supporto alla Didattica

Non previste

Bollettino

Conoscenze di base dei linguaggi di programmazione. L'insegnamento non prevede propedeuticita.

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.

L'insegnamento prevede lezioni frontali e la risoluzione in modo indipendente a casa di vari esercizi.

- 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.

Esame orale, tipicamente suddiviso in tre parti distinte.

L'esame orale verte su vari esercizi che lo studente deve svolgere in modo indipendente a casa.

H. Riis Nielson, F. Nielson, Semantics with Applications: A Formal Introduction. : Wiley, 1992

Le slide utilizzate a lezione verranno distribuite.