Guiding SMT-Based Interpolation for Program Verification

La verifica dei programmi ha un ruolo sempre più importante in ingegneria del software, e il teorema di interpolazione di Craig è al centro di numerose attività di verifica secondarie, come la computazione del fixpoint, la sommarizzazione delle funzioni e la sintesi. Per questi motivi, la capacità di costruire interpolanti adatti a scopi specifici è di grande valore pratico. Nei primi due anni di progetto abbiamo studiato l'interpolazione sia partendo dalle prove di refutazione e dal "framework di interpolazione etichettato", sia rendendo gli algoritmi di interpolazione consapevoli della struttura del codice sorgente. L'estensione del progetto approfondirà la comprensione di questi campi, con particolare riguardo alla sommarizzazione delle funzioni. Le direzioni di ricerca che vorremmo intraprendere durante i prossimi due anni includono:

(i) estendere i metodi di "prova proposizionale" e "compressione degli interpolanti" per gestire anche l'interpolazione su formule nelle teorie menzionate sopra;

(ii) estendere il framework di sommarizzazione delle funzioni basato sull'interpolazione, sviluppato da noi, da pura interpolazione proposizionale a interpolazione in SMT (satisfiability modulo theories);

(iii) la creazione di una nuova strategia di raffinazione intelligente in grado di impiegare differenti teorie su richiesta del processo di verifica;

(iv) lo sviluppo di formati per lo scambio di prove tra i diversi "interpolating solvers" e "model checkers"

Gli argomenti (i) e (ii) sono una continuazione diretta dei primi due anni del progetto.

Gli argomenti (iii) e (iv) sono testimonianza del fatto che i metodi sviluppati stanno divenendo maturi, e stanno iniziando ad essere utilizzati in applicazioni in continua evoluzione.