Home » Archivo » Archvio 2013 » ANALISI STATICA E VERIFICA DEL SOFTWARE - 2013/2014

Laurea Magistrale

Salta il menu di secondo livello

ANALISI STATICA E VERIFICA DEL SOFTWARE - 8 CFU - A.A. 2013/2014

Insegnante

Prof. Francesco Ranzato

Periodo

I Anno - 1 Trimestre | 01/10/2013 - 07/12/2013

Ore: 64 (64 lezione)

Torna su ▲

Prerequisiti

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

Conoscenze e abilità 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.

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

Attività 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

Torna su ▲