Domini astratti per la certificazione automatica di programmi (1999)

Data inizio
1 gennaio 1999
Durata (mesi) 
24
Dipartimenti
Informatica
Responsabili (o referenti locali)
Giacobazzi Roberto
URL
9901403824_001
Parole chiave
INTERPRETAZIONE ASTRATTA;ANALISI STATICA DI PROGRAMMI;VERIFICA DI PROGRAMMI;SEMANTICA

Il progetto si occupera' dello studio e della progettazione di tecniche avanzate e di strumenti effettivi per la certificazione automatica dei programmi, con particolare riferimento al caso di presenza di codice mobile. La certificazione dei programmi combina tecniche di analisi statica con le tecniche di verifica del flusso dei dati e del controllo nei programmi. La certificazione automatica e' particolarmente critica nel caso di presenza di codice mobile, in particolare per certificare la sicurezza del flusso di informazioni in programmi non certificati. L'obiettivo principale del progetto e' l'utilizzo dell'interpretazione astratta come strumento unificante per lo studio delle tecniche standard di analisi sul flusso dei dati e del controllo, dei metodi di prova, e dei metodi per l'analisi di programmi basati su tipi e su vincoli. La certificazione dei programmi rappresenta pertanto la perfetta base dalla quale partire per studiare sia gli aspetti piu' fondamentali dell'analisi e verifica dei programmi, come l'analisi di programmi parzialmente definiti e i fondamenti teorici dei domini riguardanti gli aspetti di precisione e complessita' dell'analisi, che per progettare strumenti utili per la certificazione dei programmi basata sulla semantica, strumenti che possono essere direttamente utilizzati nei moderni sistemi software per la certificazione del codice.

Enti finanziatori:

Ministero dell'Istruzione dell'Università e della Ricerca
Finanziamento: assegnato e gestito dal dipartimento
Programma: COFIN - Progetti di Ricerca di Interesse Nazionale

Partecipanti al progetto

Agostino Dovier
Roberto Giacobazzi
Professore ordinario

Attività

Strutture