Combinazione di analisi e sintesi di programmi: co-generazione di astrazioni e raffinamenti per l'analisi e la sintesi di programmi (PRIN 2009 valutato positivamente ma non finanziato)

Starting date
July 15, 2011
Duration (months)
24
Departments
Computer Science
Managers or local contacts
Giacobazzi Roberto
Keyword
INTERPRETAZIONE ASTRATTA, ANALISI STATICA, VERIFICA DI SISTEMI

Le scienze e tecnologie informatiche devono affrontare la grande sfida di sviluppare metodologie, tecnologie e strumenti adatti alla specifica dei requisiti, alla progettazione di architetture, all'implementazione, alla verifica e al test, all'utilizzo, al mantenimento e alla protezione sia durante il funzionamento che nell'evoluzione di software che sia componibile, affidabile, flessibile, scalabile e robusto. Il problema generale dell'affidabilità del software ha un enorme impatto economico: avanzamenti ed innovazioni scientifiche sono necessari per mantenere e per guadagnare porzioni di mercato. L'astrazione, come formalizzata dall'interpretazione astratta, è indispensabile nei processi di sviluppo, integrazione, verifica, analisi, testing e protezione del codice. Lo scopo del progetto AIDA2009 (che è la continuazione dei progetti AIDA2004, che raggiunse pienamente gli obiettivi, e AIDA2007, in via di completamento) è di rafforzare la ricerca italiana nell'ambito dell'interpretazione astratta, promuovendo l'interpretazione astratta come tecnologia per la costruzione di sistemi software affidabili. L'interpretazione astratta rappresenta la teoria di base per la progettazione di metodologie e per la costruzione di strumenti in grado si assicurare l'interoperabilità, la tecnologia fondamentale per software sequenziale, parallelo (sincrono e asincrono), a vincoli, distribuito e mobile che si trova in sistemi e servizi informatici, siano essi centralizzati, distribuiti o integrati. Recentemente, è stato inoltre dimostrato che l'interpretazione astratta può essere scalata ed applicata anche a complesse applicazioni industriali di grandi dimensioni. L'Europa ha indubbiamente una posizione di leadership in questa tecnologia e l'Italia ha giocato in questo campo un ruolo importante: la comunità italiana di interpretazione astratta è attiva da quasi vent'anni, ha raggiunto nell'ultimo decennio obiettivi di straordinaria importanza e, mettendo a punto soluzioni basate su interpretazione astratta di qualità industriale, sta contribuendo al processo di industrializzazione.
AIDA2009 si focalizzerà sul progetto di nuovi domini astratti e nuove integrazioni di domini, nonché su cinque filoni applicativi: l'analisi statica dei programmi, il debugging semiautomatico di programmi, la sintesi di programmi, la formalizzazione delle relazioni tra equivalenze comportamentali, e l'analisi di sistemi biologici stocastici. Nell'ambito della progettazione di domini, considereremo: la definizione di domini astratti dotati di grande scalabilità e relativamente precisi per l'analisi dei puntatori in programmi C e C++; la definizione di domini astratti numerici non relazionali per gli stessi linguaggi in grado di rappresentare insiemi non convessi e con operazioni efficienti per approssimare l'aritmetica in modulo e le operazioni bit-a-bit; la definizione di combinazioni efficaci di questi ultimi domini con i primi. Per quanto riguarda l'analisi statica di programmi, affronteremo i seguenti problemi: analisi di variabili numeriche per linguaggi imperativi utilizzando specializzazioni (dipendenti dal programma analizzato) di domini non relazionali o debolmente relazionali; analisi di sharing per linguaggi a oggetti utilizzando domini parametrici che consentono di aggiustare il rapporto costo/precisione durante l'analisi; l'analisi di problemi di planning in PDDL; l'analisi di terminazione e l'inferenza automatica di limiti superiori alla quantità di risorse utilizzate per programmi C, C++ e Java; l'integrazione di analizzatori statici con theorem prover per meccanizzare il raffinamento di astrazioni; l'analisi di inizializzazione degli array in Java. Per il debugging di programmi, studieremo l'estensione della diagnosi astratta ai linguaggi imperativi e la sua integrazione con l'analisi statica. Riguardo alla sintesi di programmi, ci occuperemo di sintesi di programmi guidata dall'astrazione e di analisi di codice metamorfo. Per quanto concerne le equivalenze comportamentali, studieremo l'uso dell'interpretazione astratta per ragionare sulle equivalenze comportamentali basate sui modelli interleaving, true-concurrent e probabilistici dei sistemi concorrenti. Nell'ambito dei calcoli per sistemi biologici, investigheremo sulle semantiche concrete e astratte per linguaggi biologici stocastici e sulla simulazione astratta di sistemi biologici stocastici.

Sponsors:

PRIN VALUTATO POSITIVAMENTE
Funds: requested
Syllabus: COFIN - Progetti di Ricerca di Interesse Nazionale

Project participants

Activities

Research facilities

Share