IRONPROOF：COBOL转Python的SMT等价性验证

Dominik Blain 发布论文提出 IRONPROOF：把 COBOL 解析为中间表示并生成 Python，再用 Z3 将两者编码为共享输入上的公式，输出可机器校验的等价性证书（UNSAT）或反例（SAT）。 在 2,345 个 COBOL 文件（GnuCOBOL 测试、NIST CCVS85、开源集合及作者自写程序）中，782 个进入检查路径：606 个（77.5%）被证明等价，101 个部分验证，无一被反驳，75 个在流程内失败并留在分母中。作者自写程序上的验证率为 92.3%，独立编写的程序上为 52.6%（291 个中 153 个）；在 AWS CardDemo 和 IBM GenApp 两个公开业务应用语料上，编码器无法端到端建模任何程序。 论文称，证明所确立的是生成的 Python 与中间表示所描述的 COBOL 行为一致，而非与 COBOL 实现本身的等价。

AI 根据报道生成 · 1 小时前更新

还没有足够的连续观测数据，暂不绘制趋势。