Quantified Formulas in Interpolating SMT Solvers

本项目的目标是开发用于量化公式的内插SMT求解器的理论和实践基础。这一目标的动机是在软件模型检查器中使用插值法。更具体地说，软件模型检查器成功地使用了内插SMT求解器来生成循环不变量的候选者，这从国际软件验证竞赛SV-COMP的几个软件模型检查器中使用内插的事实中得到了证明。作为该项目的一个结果，需要量化断言的程序类将适用于那些使用内插的软件模型检查器。这类课程实际上是相关的。例如，需要量化的断言来指定数组是排序的，或者指定散列映射中的每个元素满足数据不变量。我们将通过继续项目第一阶段的一般方法来实现这一目标，并在第一阶段获得的技术见解和结果的基础上发展。我们一般方法的一个显著特点是，我们的SMT求解器从一开始就被设计为支持内插生成，除了作为求解器具有竞争力之外。

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.