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.
