MoXIchecker: An Extensible Model Checker for MoXI
<|reference_start|>MoXIchecker: An Extensible Model Checker for MoXI: 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.<|reference_end|>
@article{ates2024moxichecker:,
    title={MoXIchecker: An Extensible Model Checker for MoXI},
    author={Salih Ates, Dirk Beyer, Po-Chun Chien, and Nian-Ze Lee},
    journal={arXiv preprint arXiv:2407.15551},
    year={2024},
    archivePrefix={arXiv},
    eprint={2407.15551},
    primaryClass={cs.SE cs.PL}
}