Analisi, verifica e sintesi di sistemi software/hardware mediante l'impiego sinergico di interpretazione astratta e ragionamento automatico (PRIN 2010-11 non finanziato)

Data inizio
1 giugno 2012
Durata (mesi) 
36
Dipartimenti
Informatica
Responsabili (o referenti locali)
Bonacina Maria Paola
Parole chiave
ANALISI E SINTESI DI PROGRAMMI, RAGIONAMENTO AUTOMATICO,INTERPRETAZIONE ASTRATTA

Metodi simbolici, quali interpretazione astratta, esecuzione simbolica, dimostrazione di teoremi, costruzione di modelli e model checking, si integrano in strumenti per rimuovere difetti nei primi stadi di sviluppo dei sistemi e sintetizzarli a partire dalle richieste degli utenti. Ogni metodo ha punti di forza e limiti, mentre la sempre crescente diversità e complessità dei sistemi software e hardware richiede sempre più l'automazione di analisi e sintesi per mantenere sostenibile
la curva qualità/costo. Questo progetto sviluppa sinergie tra interpretazione astratta e ragionamento automatico, così che i ragionatori si avvantaggino delle astrazioni e analizzatori/sintetizzatori delle prove, modelli e interpolanti generati dai ragionatori. Se dal punto di vista tecnico il progetto riguarda applicazioni interne all'informatica, il ruolo ubiquo dei sistemi software e hardware nella vita contemporanea gli dà impatto profondo e duraturo su economia e società.

Questo progetto è collegato alle tre parti di Orizzonte 2020: (1) Eccellenza nella scienza di base, (2) Competitività ed
innovazione industriale, e (3) Una società migliore. Per (1), la sfida dell'affidabilità di software e componenti è stata riconosciuta come una delle grandi sfide per la scienza del XXI secolo. Per (2), il metodo principale per la verifica del
software nell'industria è il testing, che costa molto (79 miliardi di euro globalmente nel 2010) e costerà ancor più in futuro. Verifica, analisi e sintesi di software mediante metodi simbolici non si propongono di sostituire il testing, ma completarlo e migliorarlo, riducendo i costi di sviluppo. Questo è molto importante in Italia e in Europa, dove prevalgono piccole e medie imprese, meno equipaggiate finanziariamente per sobbarcarsi i costi del testing, che si propagano dall'industria del software a tutti i rami dell'economia. Oltre ICT, aumentare affidabilità, sicurezza ed efficienza dei sistemi software e hardware ha impatto su settori chiave dell'industria e dei servizi, quali energia, trasporti, bancario, e salute. Questo porta a (3), dove l'impatto è perfino più ampio, poichè il software influenza stili di vita (comunicazione inter-personale, reti sociali), istruzione, informazione, partecipazione politica (sistemi di votazione elettronica),
gestione dei propri beni (banca in rete), e la vita di tutti i giorni. Le nostre qualità della vita, libertà e democrazia
dipendono anche dal software.

Complessità, varietà, dimensioni e pervasività del software sono tali, che nessun approccio può bastare da solo e in generale.
Una visione sempre più diffusa, e condivisa da questo progetto, è avere una sequenza di strumenti, dove tecnologie di costo
crescente si applicano a problemi di difficoltà crescente. L'interpretazione astratta compromette la precisione per l'efficienza e si applica presto. Il ragionamento automatico punta all'efficienza preservando la completezza e si applica
tardi nella sequenza. Gli spettacolari progressi in dimostrazione di teoremi, costruzione di modelli e soluzione di vincoli,
nota come "SMT big bang", ci porta a corto-circuitare la sequenza, facendo lavorare insieme interpretazione astratta e ragionamento automatico. Questa visione informa la nostra ricerca verso cinque obbiettivi:

1. Dimostrazione di teoremi per generazione automatica d'invarianti,
2. Analisi automatica di terminazione,
3. Analisi di codice metamorfico,
4. Sintesi guidata da astrazione, e
5. Compilazione sul momento a tracce.

La generazione automatica d'invarianti ci solleva dall'annotare il codice e permette agli utenti finali di partecipare alla
generazione di programmi dando solo esempi. La terminazione è fondamentale per la correttezza; l'analisi di codice metamorfico scopre software maligno (malware). La sintesi guidata da astrazione sincronizza automaticamente programmi concorrenti. La compilazione sul momento a tracce ottimizza programmi in linguaggi usati in programmazione web.




Partecipanti al progetto

Maria Paola Bonacina
Professore ordinario
Roberto Giacobazzi
Professore ordinario
Nicola Fausto Spoto
Professore associato

Collaboratori esterni

Francesco Ranzato
Università degli studi di Padova
Aree di ricerca coinvolte dal progetto
Sistemi intelligenti
Computing methodologies - Artificial intelligence

Attività

Strutture