插值法与数组性质片段
计算机科学中的逻辑
2019-04-26 v1
摘要
基于插值的软件模型检验器已成功用于自动证明程序正确。其能力来源于插值的 SMT 求解器，这些求解器检查潜在反例的可行性与计算候选不变量。该方法对无量词理论（如等式理论或线性算术）效果良好。对于带量词的公式，存在可判定带量词公式中具表达力片段的 SMT 求解器，例如 EPR、数组性质片段与有限近无解释片段。然而，这些求解器不支持插值。已知一般而言 EPR 不允许插值。本文中，我们对数组性质片段给出相同结论。
引用
@article{arxiv.1904.11381,
title = {Interpolation and the Array Property Fragment},
author = {Jochen Hoenicke and Tanja Schindler},
journal= {arXiv preprint arXiv:1904.11381},
year = {2019}
}