Quantified Formulas in Interpolating SMT Solvers

插值 SMT 求解器中的量化公式

• 批准号: 282631393
• 负责人: Dr. Jochen Hoenicke
• 金额: --
• 依托单位: Lehrstuhl Softwaretechnik
• 依托单位国家: 德国
• 项目类别: Research Grants
• 财政年份: 2015
• 资助国家: 德国
• 起止时间: 2014-12-31 至 2020-12-31
• 项目状态: 已结题
• 来源: https://gepris.dfg.de/gepris/projekt/282631393?language=en
• 关键词: Quantified; Formulas; 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.

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

项目成果

Solving and Interpolating Constant Arrays Based on Weak Equivalences

基于弱等价的常量数组求解和插值

• DOI: 10.1007/978-3-030-11245-5_14
• 发表时间: 2019
• 作者: J. Hoenicke;T. Schindler
• 通讯作者: T. Schindler