从有界检测到基于符号 up-to 技术的等价性验证
编程语言
2021-10-25 v2 计算机科学中的逻辑
摘要
我们提出一种针对带局部状态的高阶程序的限界等价性验证技术。该技术结合了类似于符号博弈语义的完全抽象符号环境双模拟、新颖的 up-to 技术，以及轻量级状态不变式标注。由此得到一种无假阳性或假阴性的等价性验证技术。该技术在限界上是完备的，即给定足够大的限界，所有不等价性均可被自动检测。此外，若干困难等价性在自动证明或经状态不变式标注后被证明。我们在名为 Hobbit 的工具原型中实现了该技术，并用一组广泛的新旧示例对其进行了基准测试。Hobbit 能够证明许多经典等价性，包括所有 Meyer 和 Sieber 示例。
引用
@article{arxiv.2105.02541,
title = {From Bounded Checking to Verification of Equivalence via Symbolic Up-to Techniques},
author = {Vasileios Koutavas and Yu-Yang Lin and Nikos Tzevelekos},
journal= {arXiv preprint arXiv:2105.02541},
year = {2021}
}