抽象解释不精确性的逻辑

《Proceedings of the ACM on Programming Languages》：A Logic for the Imprecision of Abstract Interpretations

误差传播建模与抽象解释上界推导方法研究。本文提出误差传播逻辑（EPL）解决抽象程序分析中误差累积问题，通过生成器机制限定验证范围，建立输入误差到结果误差的数学映射，实现弱局部完备性验证，并引入程序ω-连续性新逻辑。

　　

摘要AI摘要

要查看此由AI生成的摘要，您必须具有高级访问权限。

了解更多登录

摘要

摘要

在数值分析中，误差传播指的是输入数据或中间计算中的小误差如何累积并影响最终结果，这通常由算法对某些扰动的稳定性和敏感性决定。在近似程序分析中定义类似的概念仍然是一个挑战。在抽象解释中，不准确性来源于抽象本身，而这种误差的传播则由抽象解释器决定。在大多数情况下，这种不精确性是不可避免的。在本文中，我们提出了一种用于推导抽象解释不准确性（上界）的逻辑。我们能够从一个抽象解释器的输入数据的不准确性出发，推导出一个限制其结果不准确性的函数。当这种情况成立时，我们称之为抽象解释器的“部分局部完备性”，这是文献中已知的一种较弱的完备性形式。为此，我们引入了表示在抽象域中的属性的“生成器”概念。生成器允许我们在验证给定程序和输入是否满足界限函数时限制搜索空间。然后，我们引入了一种称为“误差传播逻辑”（EPL）的程序逻辑，用于传播由抽象解释产生的误差界限。这种逻辑结合了正确性和不正确性逻辑，以及本文中也介绍的“程序ω-连续性”逻辑。

AI摘要

AI生成的摘要（实验性）

该摘要是使用自动化工具生成的，并非由文章作者撰写或审阅的。它旨在帮助发现、帮助读者评估相关性，并协助来自相关研究领域的读者理解本文的工作。它旨在补充作者提供的摘要，后者仍然是文章的官方摘要。完整文章才是权威版本。点击此处了解更多。

点击此处对摘要的准确性、清晰度和实用性进行评论。您的反馈将有助于改进和未来重新生成的版本。

要查看此由AI生成的通俗语言摘要，您必须具有高级访问权限。