Domini astratti per la certificazione automatica di programmi (1999)

Starting date
January 1, 1999
Duration (months)
24
Departments
Computer Science
Managers or local contacts
Giacobazzi Roberto
URL
9901403824_001
Keyword
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.

Sponsors:

Ministero dell'Istruzione dell'Università e della Ricerca
Funds: assigned and managed by the department
Syllabus: COFIN - Progetti di Ricerca di Interesse Nazionale

Project participants

Agostino Dovier
Roberto Giacobazzi
Full Professor

Activities

Research facilities

Share