Weakly-relational shapes for numeric abstractions: improved algorithms and proofs of correctness
Weakly-relational shapes for numeric abstractions: improved algorithms and proofs of correctness
复制标题
DOI：
10.1007/s10703-009-0073-1
复制
发表时间：
2009-12
影响因子：
0.8
通讯作者：
Roberto Bagnara;P. Hill;E. Zaffanella
中科院分区：
文献类型：
--
作者：
Roberto Bagnara;P. Hill;E. Zaffanella
弱关系数值约束提供了复杂性和表达性之间的折衷，足以满足软件和硬件系统的形式分析和验证领域中的多种应用。我们提出了基于这些约束构建成熟、高效且可证明正确的抽象域所需要解决的问题。我们首先建议使用语义抽象域，其元素是几何形状，而不是先前建议所基于的约束网络和矩阵的（更具体的）句法抽象域。这可以一劳永逸地解决以下问题：蕴含闭包（实现此类域的关键操作）似乎阻碍了适当的扩展算子的实现。在我们的方法中，加宽的实现依赖于所考虑的约束描述的有效归约程序的可用性：文献中已经存在有界差分形状域的归约程序；我们为有理数和整数八边形形状的更复杂的情况提供算法。我们还通过提出基于有理和整数八边形约束的域降低复杂性的蕴涵算法及其正确性证明来改进最先进的技术。还讨论了使用浮点数实现弱关系数值域的后果。
Weakly-relational numeric constraints provide a compromise between complexity and expressivity that is adequate for several applications in the field of formal analysis and verification of software and hardware systems. We address the problems to be solved for the construction of full-fledged, efficient and provably correct abstract domains based on such constraints. We first propose to work withsemanticabstract domains, whose elements aregeometric shapes, instead of the (more concrete) syntactic abstract domains of constraint networks and matrices on which the previous proposals are based. This allows to solve, once and for all, the problem wherebyclosure by entailment, a crucial operation for the realization of such domains, seemed to impede the realization of proper widening operators. In our approach, the implementation of widenings relies on the availability of an effective reduction procedure for the considered constraint description: one for the domain ofbounded difference shapesalready exists in the literature; we provide algorithms for the significantly more complex cases of rational and integeroctagonal shapes. We also improve upon the state-of-the-art by presenting, along with their proof of correctness, closure by entailment algorithms of reduced complexity for domains based on rational and integer octagonal constraints. The consequences of implementing weakly-relational numerical domains with floating point numbers are also discussed.