Presentazione

Organizzazione della Didattica

DM270
INFORMATICA ORD. 2014


6

Corsi comuni

 

Frontali Esercizi Laboratorio Studio Individuale
ORE: 48 0 0 136

Periodo

AnnoPeriodo
I anno1 semestre

Frequenza

Facoltativa

Erogazione

Convenzionale

Lingua

Inglese

Calendario Attività Didattiche

InizioFine
01/10/201620/01/2017

Tipologia

TipologiaAmbitoSSDCFU
caratterizzanteDiscipline informaticheINF/016


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

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 e/o lo sviluppo di un progetto di verifica del software.

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

Esame orale e/o progetto software, possibilmente suddivisi in parti distinte.

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.

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

Le slide utilizzate a lezione verranno distribuite.