Quantified Formulas in Interpolating SMT Solvers

点击翻译按钮获取中文摘要

The goal of this project is to develop the theoretical and practical foundations of an interpolating SMT solver for quantified formulas. This goal is motivated by the use of interpolation in software model checkers. More specifically, software model checkers successfully employ interpolating SMT solvers to generate candidates for loop invariants.This is witnessed by the fact that interpolation is used in several of the software model checkers in SV-COMP, an international software verification competition. As an outcome of the project, the class of programs that require quantified assertions will be in reach for those software model checkers using interpolation. This class of programs is practically relevant. Quantified assertions are needed, for example, to specify that an array is sorted or to specify that each element in a hash map satisfies a data invariant.We will accomplish the goal by continuing the general approach of the first phase of the project, building up on the technical insights and results which we have obtained in the first phase. A distinguishing feature of our general approach is that our SMT solver is designed from the start to support interpolant generation, in addition to being competitive as a solver.