Guiding SMT-Based Interpolation for Program Verification

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 we have developed from purely propositional interpolation to interpolation in ssatisfiability modulo 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 solvers and 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 gainig maturity and are starting to be used more in evolving applications.