Verifying a Local Generic Solver in Coq
Verifying a Local Generic Solver in Coq
复制标题
在 Coq 中验证本地通用求解器
DOI：
10.1007/978-3-642-15769-1_21
复制
发表时间：
2010
期刊：
影响因子：
--
通讯作者：
Helmut Seidl
中科院分区：
文献类型：
--
作者：
Martin Hofmann;Aleksandr Karbyshev;Helmut Seidl
不动点引擎是程序分析工具和编译器的核心组件。如果这些工具是值得信赖的，还应特别注意这些求解器的正确性。本文考虑了局部通用不动点求解器RLD，它可以应用于约束系统，在某些格上，其中右端f x是用某种规范语言实现的任意函数。该算法的验证具有挑战性，因为它使用高阶函数，并依赖于副作用来跟踪变量依赖性，因为它们在定点迭代期间动态遇到。在这里，我们提出了一个正确性证明，该算法已被形式化的交互式证明assistantCoq。
Fixpoint engines are the core components of program analysis tools and compilers. If these tools are to be trusted, special attention should be paid also to the correctness of such solvers. In this paper we consider the local generic fixpoint solverRLDwhich can be applied to constraint systems, over some latticewhere the right-hand sidesfxare given as arbitrary functions implemented in some specification language. The verification of this algorithm is challenging, because it uses higher-order functions and relies on side effects to track variable dependences as they are encountered dynamically during fixpoint iterations. Here, we present a correctness proof of this algorithm which has been formalized by means of the interactive proof assistantCoq.
登录
查看更多内容
一般方程组的更快求解器
影响因子：
1.3
作者：
Christian Fecht;H. Seidl
通讯作者：
H. Seidl
建构性逻辑
影响因子：
1.5
作者：
Thierry Coquand;P. Schuster;I. Yengui
通讯作者：
I. Yengui
使用需求分析和混沌迭代在有限函数空间中查找不动点
DOI：
10.1007/3-540-58485-4_50
发表时间：
1994
期刊：
Nord. J. Comput.
影响因子：
--
作者：
Niels Jørgensen
通讯作者：
Niels Jørgensen
消除程序逻辑中的幽灵变量
影响因子：
2.9
作者：
M. Hofmann;M. Pavlova
通讯作者：
M. Pavlova
什么是纯函数？
DOI：
10.1007/978-3-642-14162-1_17
发表时间：
2010
期刊：
影响因子：
--
作者：
Martin Hofmann;Aleksandr Karbyshev;Helmut Seidl
通讯作者：
Helmut Seidl