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. 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 AIDA2007 -- che è la continuazione del progetto AIDA2004 che raggiunse pienamente gli obiettivi - è 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 composizionalità, la scalabilità, l'affidabilità, la robustezza, la sicurezza e l'auto-adattamento del software. Si è dimostrato come l'interpretazione astratta sia una 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. AIDA2007 si focalizzerà sullo sviluppo di metodologie fondazionali e su tre filoni di applicazioni: l'analisi statica dei programmi, la protezione del codice e la verifica dei sistemi. Nell'ambito delle metodologie fondazionali, considereremo la progettazione sistematica di domini ottimali per il model checking, la definizione di domini astratti per l'analisi di puntatori e di aliasing per programmi C e Java, la progettazione di domini astratti numerici che siano scalabili e precisi, lo sviluppo di metodi sistematici per misurare la precisione dell'analisi che integrano nei domini astratti dell'informazione probabilistica e statistica, e la definizione di trasformazioni semantiche che permettano di ottenere proprietà di completezza. Per quanto riguarda l'analisi statica di programmi, affronteremo i seguenti problemi: specifica ed analisi di proprietà causali in sistemi concorrenti e distribuiti,
> ottimizzazione speculativa, analisi di terminazione e complessità di programmi C e Java mediante interpretazione astratta, definizione di astrazioni numeriche modulari, estensione di linguaggi mediante annotazioni nelle fasi di sviluppo e analisi del codice, analisi precise di string cleanness. Nell'ambito della protezione del codice, studieremo il problema di nascondere informazione nei linguaggi di programmazione, con particolare attenzione al software watermarking, alla protezione del copyright, all'offuscamento di codice per impedire il reverse engineering e all'identificazione di malware in presenza di malware metamorfici (ovvero offuscati). Per quanto riguarda la verifica automatica di sistemi, studieremo algoritmi di raffinamento delle astrazioni per il model checking astratto, trasformazioni di linguaggi temporali per ottenere la preservazione forte rispetto ad una data astrazione, e algoritmi efficienti basati su interpretazione astratta per calcolare equivalenze comportamentali in algebre di processi.
