面向 MDP 的 IEEE 754 浮点实现的区间迭代形式化验证
计算机科学中的逻辑
2025-10-07 v3
摘要
我们提出了一个高效可执行的、针对区间迭代的形式化验证实现。我们的正确性证明涵盖从 MDP 高级抽象语义到基于浮点算术的 LLVM 低层实现的整个开发过程。我们使用 Isabelle/HOL 证明助手验证区间迭代的收敛性,并采用分步骤细化方法推导出高效的 LLVM 代码实现。为此,我们扩展了 Isabelle 细化框架,以支持对浮点算术和定向舍入模式的推理。我们在实验中表明,该验证实现在竞争性地与 MDP 的最先进工具相当,同时提供对结果正确性的形式化保证。
引用
@article{arxiv.2501.10127,
title = {A Formally Verified IEEE 754 Floating-Point Implementation of Interval Iteration for MDPs},
author = {Bram Kohlen and Maximilian Schäffeler and Mohammad Abdulaziz and Arnd Hartmanns and Peter Lammich},
journal= {arXiv preprint arXiv:2501.10127},
year = {2025}
}