L'interpretazione astratta e' una teoria generale per l'approssimazione di sistemi dinamici, ampiamente utilizzata ad esempio per derivare formalmente strumenti di analisi statica e verifica di programmi a partire dalla loro semantica. In AIDA, l'interpretazione astratta e' vista come teoria fondamentale ed unificante per la progettazione di metodologie e lo sviluppo di strumenti per assicurare l'interoperabilita', la composizionalita', l'affidabilita', la robustezza, e la sicurezza di sistemi software. L'obiettivo iniziale del progetto AIDA e' di mobilitare, unificare, galvanizzare e rafforzare la comunita' italiana dell'interpretazione astratta attraverso un obiettivo comune che consiste nella realizzazione di un'unica piattaforma avanzata per la certificazione di sistemi attraverso interpretazione astratta. Siamo particolarmente interessati alla certificazione di flussi sicuri di informazione, robustezza e affidabilita' di sistemi complessi che coinvolgono componenti software e che hanno un potenziale comportamento ibrido. Affronteremo questo problema raffinando gli esistenti metodi propri dell'interpretazione astratta nell'ambito dell'analisi statica di programmi e nella sicurezza, integrandole con descrizioni basate sui vincoli di sistemi dal numero infinito di stati e metodi di verifica come il model checking. Il risultato verra' ottenuto individuando un modello comune per la progettazione dell'interpretazione astratta nell'analisi statica do programmi, nella sicurezza, nel testing, nei sistemi ibridi, nei vincoli e nella verifica automatica. L'interpretazione astratta fornisce in questo caso un framework comune, dove problemi derivanti da diversi aspetti della certificazione di sistemi, che possono essere profondamente diversi come natura e applicazione, possono essere integrati, arricchiendo di nuovi strumenti l'interpretazione astratta teorica e pratica. La certificazione automatica di sistemi sia per sistemi dinamici discreti che per sistemi ibridi rappresenta il contesto ideale sia per studiare nuovi aspetti fondamentali dell'interpretazione astratta, come la teoria dei domini, la precisione e la complessita' dell'analisi statica di programmi, sia per fornire utili strumenti per la certificazione di sistemi basati sulla semantica che possono essere direttamente utilizzati nei moderni sistemi software.
