.png){kind=icon}
返回
A program instrumentation framework for automatic verification
.png){kind=icon}
PRE
AI
DOI：10.1007/s10703-026-00493-w.png)
.png){kind=icon}
.png){kind=icon}
分享.png){kind=icon}
收藏
摘要
En 中文
在演绎验证和软件模型检测中，当后端求解器不够强大或缺乏所需理论时，处理某些规范语言构造可能会出现问题。一种解决方法是，为了验证目的，将程序转换为不使用这些有问题的构造的等价程序，并对这个等价程序进行推理。在本文中，我们提出程序插桩作为统一的验证范式，它涵盖了各种现有的特定方法，具有明确的正式正确性标准，可以自动应用，并且能够传递回证据和反例。我们通过自动验证涉及数组的量化和聚集操作的程序来说明我们的方法，例如数组给定段中的最大值或元素和，这些操作已知难以自动推理。我们在MonoCera工具中实现了我们的方法，该工具专门用于验证具有聚集操作的程序，并在示例程序（包括SV-COMP程序）上对其进行了评估。
Keyword:
Program instrumentation
Automatic verification
Ghost code
期刊
F
IF:
0.8
论文数:
11
被引数:
0
机构
查看更多机构
引用论文
暂无论文信息