MoXIchecker：面向MoXI的可扩展模型检查器

MoXI 是 2024 年引入的一种新的中间验证语言，用于通过扩展 SMT-LIB 2 语言引入状态转换系统的定义构造，促进符号模型检查的标准化和开源实现。MoXI 工具套件提供了从 MoXI 到 Btor2 的翻译器，后者是硬件验证的低级中间语言，以及基于翻译的模型检查器，该检查器调用成熟的 Btor2 硬件模型检查器来分析翻译后的验证任务。由于将 MoXI 翻译到较低级语言，更复杂的理论（如整数或实数算术）无法用固定长度的位向量精确表达，因此翻译基于的可扩展性受到限制。我们提出了 MoXIchecker，即第一个直接解决 MoXI 验证任务的模型检查器。与翻译到较低级语言不同，MoXIchecker 使用 solver-agnostic 库 PySMT 作为其验证算法的后端。由于能够容纳涉及更复杂理论的验证任务（不受较低级语言限制），便于实现新的算法，并且通过使用 PySMT 的 API 实现 solver-agnostic，因此 MoXIchecker 是可扩展的。在我们的评估中，MoXIchecker 唯一解决了使用整数或实数算术的任务，并且在性能上与 MoXI 工具套件中的翻译基于模型检查器相当。