MoXI is a new intermediate verification language introduced in 2024 to promote the standardization and open-source implementations for symbolic model checking by extending the SMT-LIB 2 language with constructs to define state-transition systems. The tool suite of MoXI provides a translator from MoXI to Btor2, which is a lower-level intermediate language for hardware verification, and a translation-based model checker, which invokes mature hardware model checkers for Btor2 to analyze the translated verification tasks. The extensibility of such a translation-based model checker is restricted because more complex theories, such as integer or real arithmetics, cannot be precisely expressed with bit-vectors of fixed lengths in Btor2. We present MoXIchecker, the first model checker that solves MoXI verification tasks directly. Instead of translating MoXI to lower-level languages, MoXIchecker uses the solver-agnostic library PySMT for SMT solvers as backend for its verification algorithms. MoXIchecker is extensible because it accommodates verification tasks involving more complex theories, not limited by lower-level languages, facilitates the implementation of new algorithms, and is solver-agnostic by using the API of PySMT. In our evaluation, MoXIchecker uniquely solved tasks that use integer or real arithmetics, and achieved a comparable performance against the translation-based model checker from the MoXI tool suite.

翻译：MoXI是2024年提出的一种新型中间验证语言，旨在通过扩展SMT-LIB 2语言以支持状态转移系统的定义，从而促进符号模型检验的标准化与开源实现。MoXI工具套件提供了从MoXI到硬件验证底层中间语言Btor2的转换器，以及一个基于转换的模型检验器——该检验器通过调用成熟的Btor2硬件模型检验器来分析转换后的验证任务。此类基于转换的模型检验器的可扩展性受限，因为更复杂的理论（如整数或实数算术）无法通过Btor2中固定长度的位向量精确表达。本文提出MoXIchecker，这是首个直接求解MoXI验证任务的模型检验器。MoXIchecker不再将MoXI转换为底层语言，而是采用与求解器无关的PySMT库作为其验证算法的后端SMT求解器。该工具具有高度可扩展性：既能处理涉及复杂理论的验证任务（不受底层语言限制），又便于新算法的实现，同时通过PySMT的API保持与求解器的无关性。实验评估表明，MoXIchecker能够唯一地求解使用整数或实数算术的验证任务，并在性能上与MoXI工具套件中的基于转换的模型检验器达到相当水平。