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