Accelerated bounded model checking with LoAT

doi:10.1016/j.scico.2026.103497

2026-08-01

Frohn, Florian *

Jürgen Giesl

DOI：10.1016/j.scico.2026.103497

原文链接

查看原文

摘要

En 中文

LoAT是一个完全自动化的验证工具，可以证明线性约束Horn子句的可满足性（或不满足性），以及转换系统的非终止性和最坏情况运行时复杂度的下界。最近，我们介绍了加速有界模型检测（ABMC），这是一种结合了加速技术与有界模型检测（BMC）的新型模型检测技术，并将其实现在LoAT中。加速技术计算“捷径”，将许多执行步骤“压缩”为单个步骤，因此ABMC能够找到BMC难以发现的深层反例，因为使用BMC找到这些反例需要较大的界限。

Keyword:

CHCs

Safety

Bounded model checking

Acceleration