MoXIchecker: An Extensible Model Checker for MoXI
Salih Ates, Dirk Beyer, Po-Chun Chien, and Nian-Ze Lee

TL;DR
MoXIchecker is a novel, extensible model checker that directly verifies MoXI language tasks using SMT solvers, overcoming limitations of translation-based approaches and supporting complex theories like integer and real arithmetic.
Contribution
It introduces MoXIchecker, the first model checker for MoXI that directly handles complex theories and is solver-agnostic, enhancing extensibility and expressiveness.
Findings
MoXIchecker successfully verifies tasks with integer and real arithmetic.
It performs comparably to existing translation-based model checkers.
It demonstrates extensibility by supporting complex theories beyond bit-vectors.
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…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsModel-Driven Software Engineering Techniques · Real-Time Systems Scheduling · Parallel Computing and Optimization Techniques
