---

Abstract

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.

Reproduction Information

MoXIchecker 0.2 was used for the evaluation presented in the paper and its source code is available on GitLab and Zenodo. The benchmark tasks can be found in a separate repository. To ensure reliable resource measurement and reproducible results, BenchExec (at this commit) was employed for running the experiments.

Experimental Results

The experimental results of RQ1 reported in the paper are available on this interactive HTML page. You can click on the cells in the status columns to see the respective log output and navigate through the tabs to view various plots. In addition, you can click on the preconfigured links below to view the corresponding tables and figures.

• Table 1
• Figure 4
• Figure 5
• Figure 6