next up previous contents
Next: Fondamenti dell'Informatica: semantica e Up: PROFILO Metodi formali Previous: PROFILO Metodi formali   Indice

Metodi Formali: analisi e verifica di programmi

Un aspetto fondamentale della moderna scienza dei calcolatori è quello di fornire strumenti per poter ragionare sulle proprietà dei programmi. Le proprietà più interessanti sono quelle legate alla semantica dei programmi, ovvero a ciò che i programmi fanno indipendentemente dalla loro rappresentazione in un dato linguaggio di programmazione. Ad esempio, nei moderni sistemi disptribuiti WWW è spesso necessario assicurare un corretto e sicuro flusso di informazioni affinchè non vengano violate privacy o venga compromessa la sicurezza dei sistemi di elaborazione. Analogamente, nei compilatori è importante conoscere il flusso delle informazioni all'interno delle varie strutture del programma (ovvero la semantica del programma) per potere trasformare questo al fine di ottenere un programma semanticamente equivalente ma migliore in prestazioni. Questi problemi sono risolti da strumenti largamente utilizzati nei moderni browsers e compilatori per verificare ed ottimizzare il codice importato dall'esterno o prodotto in fase di compilazione. Tuttavia, la natura indecidibile dei problemi legati alla semantica dei linguaggi di programmazione, impone una necessaria approssimazione nella fase di analisi e verifica formale.

Nel corso vengono studiati i principali metodi formali per costruire sistematicamente strumenti per l'analisi statica e la verifica automatica di correttezza di programmi scritti in un linguaggio di programmazione (qualunque esso sia) mediante tecniche di approssimazione semantica. A partire da una semantica molto concreta (vicina all'esecuzione reale dei programmi) di un generico linguaggio di programmazione, verranno definite semantiche via via più astratte, a partire dalla semantica denotazionale per finire con la progettazione di analizzatori statici e strumenti di verifica automatica di programmi.


Programma del corso:

Definizioni induttive

Semantica operazionale dei linguaggi di programmazione
Strutture algebriche di base

Reticoli, CPO e Domini
Teoremi di punto fisso (Knaster-Tarski)
Esempio: Semantica delle tracce massimali finite ed infinite
Esempio: Semantica denotazionale di un linguaggio funzionale
Approssimazione semantica e interpretazione astratta

Connesioni di Galois e Domini astratti
Approssimazione di punto fisso e teoremi di trasferimento
Semantica denotazionale

Semantica denotazionale come astrazione da una semantica delle tracce
Determinismo/non-determinismo
Analisi statica e verifica

Analisi sul flusso dei dati e sintesi automatica di asserzioni
Principali domini astratti per l'analisi sul valore dei dati
Analisi degli intervalli ed estrapolazione dei punti fissi
Analisi delle relazioni lineari (cenni)
Analisi di aliasing
Analisi di sicurezza
Struttura delle astrazioni

Il reticolo delle interpretazioni astratte

Testi consigliati: articoli scientifici e materiale fornito dal docente.

Titolare del Corso: Prof. Roberto Giacobazzi.


next up previous contents
Next: Fondamenti dell'Informatica: semantica e Up: PROFILO Metodi formali Previous: PROFILO Metodi formali   Indice
Roberto Giacobazzi
1999-07-20