Project

Back to overview

Guiding SMT-Based Interpolation for Program Verification

English title Guiding SMT-Based Interpolation for Program Verification
Applicant Sharygina Natasha
Number 163001
Funding scheme Project funding (Div. I-III)
Research institution Istituto del Software (SI) Facoltà di scienze informatiche
Institution of higher education Università della Svizzera italiana - USI
Main discipline Mathematics
Start/End 01.03.2016 - 28.02.2018
Approved amount 338'184.00
Show all

All Disciplines (2)

Discipline
Mathematics
Information Technology

Keywords (2)

Interpolation-based Model Checking; Formal Verification

Lay Summary (Italian)

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.

Direct link to Lay Summary Last update: 26.02.2016

Responsible applicant and co-applicants

Employees

Publications

Publication
Duality-based interpolation for quantifier-free equalities and uninterpreted functions
Leonardo Alt Antti Eero Johannes Hyvärinen Sepideh Asadi Natasha Sharygina (2017), Duality-based interpolation for quantifier-free equalities and uninterpreted functions, in 2017 Formal Methods in Computer Aided Design, {FMCAD} 2017, Vienna, Austria, October .
HiFrog: SMT-based Function Summarization for Software Verification
Leonardo Alt Sepideh Asadi Hana Chockler Karine Even-Mendoza Grigory Fedyukovich Antti E. J. Hy (2017), HiFrog: SMT-based Function Summarization for Software Verification, in Tools and Algorithms for the Construction and Analysis of Systems .
LRA Interpolants from No Man's Land
Leonardo Alt and Antti E. J. Hyvarinen Natasha Sharygina (2017), LRA Interpolants from No Man's Land, in Hardware and Software: Verification and Testing - 13th International Haifa Verifiicati.
Theory Refinement for Program Verification.
Antti E. J. Hyvärinen Sepideh Asadi Karine Even-Mendoza Grigory Fedyukovich Hana Chockler Natas (2017), Theory Refinement for Program Verification., in SAT 2017 conference.

Collaboration

Group / person Country
Types of collaboration
Formal methods group, Politecnico di Torino Italy (Europe)
- in-depth/constructive exchanges on approaches, methods or results
- Publication
- Research Infrastructure
Software Engineering Institute, Carnegie Mellon University United States of America (North America)
- in-depth/constructive exchanges on approaches, methods or results
- Publication
- Exchange of personnel
Microsoft Research (MSR), Redmond, U.S.A United States of America (North America)
- in-depth/constructive exchanges on approaches, methods or results
- Publication
- Research Infrastructure
- Exchange of personnel

Scientific events

Active participation

Title Type of contribution Title of article or contribution Date Place Persons involved
FMCAD 2017 Student Forum Poster HiFrog: Interpolation-based Software Verification using Theory Refinement 19.09.2017 Vienna, Austria Asadi Sepideh; Sharygina Natasha; Alt Leonardo; Hyvarinen Antti;
11th Alpine Verification Meeting (AVM 2017) Individual talk HiFrog: SMT-based Function Summarization for Software Verification 10.05.2017 Visegrád, Hungary Sharygina Natasha; Asadi Sepideh; Alt Leonardo; Hyvarinen Antti;


Knowledge transfer events

Active participation

Title Type of contribution Date Place Persons involved
Haifa Verification at IBM Workshop 23.11.2016 Haifa, Israel Hyvarinen Antti; Alt Leonardo; Asadi Sepideh; Sharygina Natasha;


Associated projects

Number Title Start Funding scheme
138078 Quality of Interpolants in Model Checking 01.05.2013 Project funding (Div. I-III)
138078 Quality of Interpolants in Model Checking 01.05.2013 Project funding (Div. I-III)

Abstract

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.
-