Projekt

Disziplin

Interpolation-based Model Checking; Formal Verification

Lead
Guiding SMT-Based Interpolation for Program Verification,Prof. Natasha Sharygina
Lay summary
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.

Direktlink auf Lay Summary

Letzte Aktualisierung: 26.02.2016

Aktiver Beitrag

Aktiver Beitrag

Nummer	Titel	Start	Förderungsinstrument

This proposal describes a request of extension to a previous SNF funded project #200021-138078 on Quality of Interpolants in Model Checking. The first two years of the project resulted in a book chapter, four technical publications (with three more publications being currently under review for high-profile conferences), development of two new tools, and a significant further development of two other tools. The strong theoretical, technical and experimental results confirm the feasibility of the ideas from the original proposal and we believe that the success achieved during the first two years of the project justifies the work proposed in this proposal.Software verification has an increasingly important role in software engineering, and interpolation is at the core of several verification subtasks such as fixpoint computation, function summarization and synthesis. Capability of constructing interpolants that are suitable for a particular purpose is therefore of great practical value. In the first two years of the project we have studied interpolation both starting from the refutation proof and the Labeled Interpolation System framework and by making the interpolation algorithms aware of the source code structure. In this extension we plan to deepen the understanding in these fields in particular in connection with function summaries. The directions we would study during the next two years include (i) extending the propositional proof and interpolant compression methods to handle also interpolation over formulas in the above mentioned theories;(ii) extending the successful interpolation based function summarization framework wehave developed from purely propositional interpolation to interpolation in ssatisfiabilitymodulo theories;(iii) creating an intelligent refinement strategy capable of employing different theories on demand as the verification process advances; and(iv) developing formats for exchanging proofs between different interpolating solversand model checkers.The topics (i) and (ii) are a direct continuation of the first two years of the project.The topics (iii) and (iv) are reflecting the fact that the developed methods are gainigmaturity and are starting to be used more in evolving applications.