论文标题
连续阵列的一般插值和强融合
General Interpolation and Strong Amalgamation for Contiguous Arrays
论文作者
论文摘要
插值是软件验证中的重要工具，其中一阶理论用于约束程序操纵程序。在本文中，我们介绍了与Maxdiff连续数组的数据类型理论，其中阵列在其分配内存中完全定义，Maxdiff为此返回了它们不同的最大索引。该理论比以前研究的阵列理论更具表现力。通过通过代数分析表明其模型强烈合并，我们证明该理论可以接受无量词的插值，尤其是插值转移到理论组合中。最后，我们提供了一种显着改善相关阵列理论的算法：它依赖于线性算术中的一般插值的多元化减少，从而避免了不切实际的完整术语实例实例化和无界环。
Interpolation is an essential tool in software verification, where first-order theories are used to constrain datatypes manipulated by programs. In this paper, we introduce the datatype theory of contiguous arrays with maxdiff, where arrays are completely defined in their allocation memory and for which maxdiff returns the max index where they differ. This theory is strictly more expressive than the array theories previously studied. By showing via an algebraic analysis that its models strongly amalgamate, we prove that this theory admits quantifier-free interpolants and, notably, that interpolation transfers to theory combinations. Finally, we provide an algorithm that significantly improves the ones for related array theories: it relies on a polysize reduction to general interpolation in linear arithmetics, thus avoiding impractical full terms instantiations and unbounded loops.
