“Analizzare le analisi di programma (ASPRA)" - PRIN 2017

“Analizzare le analisi di programma (ASPRA)
  dal 01/01/19 al 01/01/20
“Analizzare le analisi di programma (ASPRA)”, coordinato da Roberto Giacobazzi, docente del dipartimento di Informatica, è tra i progetti dell’università di Verona finanziati dal bando Prin 2017.

Il programma Prin è destinato al finanziamento di progetti di ricerca pubblica, allo scopo di favorire il rafforzamento delle basi scientifiche nazionali e rendere più efficace la partecipazione alle iniziative relative ai Programmi Quadro dell’Unione Europea. Il meccanismo di assegnazione dei fondi del Miur è basato su precisi principi guida: l’alto profilo scientifico del coordinatore nazionale e dei responsabili di unità operativa; l’originalità, adeguata metodologia, impatto e fattibilità del progetto di ricerca; la finanziabilità dei progetti in ogni campo di ricerca; un adeguato sostegno finanziario garantito dal Miur.

L'idea di programmi che certificano altri programmi si deve ad A.M. Turing (1949), e venne in seguito portata avanti da J. McCarthy, R.W. Floyd e C.A.R. Hoare negli anni '60. Negli ultimi cinquant’anni c’è stata un'incredibile fioritura di metodi e strumenti per raggiungere questo ambizioso obiettivo. Tra questi vi sono i compilatori certificati, i verificatori di tipo, i verificatori di modelli software e le analisi statiche di programma basate sull'interpretazione astratta.
A grandi linee è possibile fare una distinzione tra l’approccio induttivo e quello coinduttivo. L'interpretazione astratta è tra le tecniche di maggior successo del primo approccio, mentre la bisimulazione è storicamente la tecnica preferita del secondo. Oggi la coinduzione è un concetto importante in diversi campi, come nella teoria degli automi, nella teoria dei tipi, e nella teoria della prova con applicazioni in compilatori e proof assistant. La nozione di astrazione è centrale in entrambe le impostazioni: essa permette infatti di rendere possibile l'analisi del programma e di semplificare le prove coinduttive tramite le cosiddette tecniche up-to. L'idea è quella di approssimare la semantica di un linguaggio di programmazione interpretando il codice su un dominio che rappresenta solo alcune proprietà di interesse, chiamate dominio astratto. Nell'analisi dei programmi la tensione principale si ha tra la scalabilità – tipicamente ottenuta attraverso domini semplici – e la precisione, in genere ottenuta attraverso domini più raffinati, che di norma determinano un onere computazionale. Nella verifica con tecniche up-to la tensione principale sta nella possibilità di avere ancora una prova semplificata di correttezza utilizzando un linguaggio di affermazioni astratte. Questi fenomeni dipendono fortemente dalla scelta dell'astrazione e dal modo in cui il codice è scritto. Mentre il primo aspetto è stato notevolmente studiato fin dalle origini dell'interpretazione astratta alla fine degli anni '70, il secondo ha ricevuto poca attenzione e rappresenta ancora oggi una grande sfida che va alle radici della nostra disciplina.
L'antitesi Church-Turing è lo spazio bidimensionale attraversato dai due assi coordinati dell'informatica: l'asse delle funzioni e l'asse dei programmi. Il primo è ottenuto dalla visione estensiva del calcolo come elaborazione dei dati. Il secondo fornisce invece la visione intensionale del calcolo come processo controllato. La visione estensiva cattura ciò che è il risultato del calcolo; la visione intensionale cattura invece i meccanismi sottostanti, come la complessità tempo/spazio o le proprietà del flusso di dati/controllo. Questa antitesi estensionale/intensionale è al centro dell'informatica come disciplina scientifica e dipende dai livelli di astrazione sul comportamento osservabile del sistema in analisi. Così come per la complessità computazionale, il modello standard di computabilità non è adatto per ragionare sulla precisione delle analisi e delle verifiche. Programmi estensionalmente equivalenti ma intensionalmente diversi possono produrre risultati diversi quando vengono analizzati o verificati.

Il progetto ASPRA ha lo scopo di sperimentare un nuovo metodo per migliorare l'analisi e la verifica dei programmi, fornendo un progresso fondamentale nella comprensione della struttura e delle proprietà dei programmi per i quali un’analisi è precisa. L'obiettivo generale di ASPRA è quello di sviluppare una teoria completa che spieghi la natura della precisione delle analisi e dei metodi di verifica automatizzati e semi-automatizzati dei programmi, con l'obiettivo di fornire metodi e strumenti per la messa a punto della precisione dell'analisi e della verifica dei programmi, eventualmente agendo a livello sintattico sulle strutture del codice. ASPRA vuole dare una risposta ad un'esigenza emergente nella programmazione. Assistiamo ad una progressiva espansione del programmare, con una tendenza che va verso l'idea che "scrivere codici sarà qualcosa che praticamente tutti faranno ogni giorno" (Peter Lee 2015). Questo dovrebbe riflettersi sul modo in cui progettiamo strumenti per l'analisi e la verifica dei programmi. La progettazione di astrazioni precise per una lunga serie di programmi è estremamente costosa. La rielaborazione del codice per affrontare meglio una certa analisi può essere un'alternativa più economica e accessibile.
Il progetto ASPRA prevede di sfruttare la natura intensionale della precisione dell'analisi e della verifica dei programmi. Il nostro obiettivo è quello di estendere i metodi standard di estensione – proof methods e teoria della ricorsione - da una prospettiva intensionale, con particolare enfasi su come la precisione dell'analisi e della verifica del programma è influenzata dal modo in cui il codice è scritto. Saranno considerati e messi in relazione tra loro sia i metodi di prova induttivi che quelli coinduttivi. Prevediamo di sviluppare metodi e strumenti induttivi e coinduttivi per analizzare le analisi dei programmi al fine di migliorarne la precisione agendo sulle strutture del codice (ad esempio, attuando un refactoring delle trasformazioni del codice), con applicazioni nell'analisi dei programmi, analisi dei programmi probabilistici, nella sicurezza linguistica e in proof assistant. I risultati attesi avranno per lo più un impatto fondamentale nella comprensione del modo in cui l'analisi del programma reagisce una volta che la struttura intensionale del codice in osservazione viene modificata.

Organizzazione

Strutture del dipartimento

Condividi