kMoXI

SMT-based model checker for MoXI, the Model eXchange Interlingua, built on the engines of Kind 2

About

kMoXI (kmoxi) is a model checker for MoXI, the Model eXchange Interlingua, a language for symbolic model checking of transition systems built on SMT-LIB. It is a second executable built from the sources of Kind 2: a MoXI front end on top of the engines of Kind 2, which run in parallel on the transition system of the model. A model declares its logic, defines one or more systems and checks one of them with a check-system command; kMoXI answers each query with a MoXI check-system-response: unsat when no execution satisfies the query, with the inductive invariant that proves it as a certificate, or sat, with a witnessing trace.

Main features

Native MoXI input (the S-expression syntax), checked against the MoXI language definition before the analysis
Logics QF_BV, QF_ABV, QF_LIA, QF_ALIA, QF_LRA and QF_NIA
Multiple model checking engines, run in parallel and sharing their invariants:
- Bounded Model Checking (BMC)
- k-induction
- IC3 with quantifier elimination or with implicit abstraction
- Invariant generation
Certificates (inductive invariants) for unsat answers and traces for sat answers, in the MoXI response format
Several queries per check-system command, answered in order
Support for multiple SMT solvers as backend reasoning engines
- Bitwuzla, cvc5, MathSAT5, SMTInterpol, Yices 2, and Z3

Building

kMoXI is not distributed with the Kind 2 releases or through OPAM. It is built from a clone of the Kind 2 repository, with the same dependencies as Kind 2:

git clone https://github.com/kind2-mc/kind2.git
cd kind2
make kmoxi

This builds and installs bin/kmoxi. kMoXI has a version of its own, independent of that of Kind 2; kmoxi --version prints it with the Kind 2 build it comes from. See the building instructions in the README for the dependencies and the supported solvers.

Usage

kmoxi [options] model.moxi

For example, the following model checks whether the counter of system counter can reach the value 10:

(set-logic QF_LIA)
(define-system counter
  :input ((reset Bool))
  :output ((c Int))
  :init (= c 0)
  :trans (= c' (ite reset 0 (+ c 1))))
(check-system counter
  :input ((reset Bool))
  :output ((c Int))
  :reachable (ten (= c 10))
  :query (reach_ten (ten)))

kMoXI answers sat for the query reach_ten, with a trace of eleven states in which reset stays false. Useful options, all shared with Kind 2, include --timeout, --enable to run selected engines only, and --smt_solver and its companions to choose the solvers; kmoxi --help lists them. The usage section of the README describes the response format and the certificates, and the supported subset of MoXI.

Documentation

kMoXI in the Kind 2 README: building, usage, and the supported subset of MoXI
MoXI: An Intermediate Language for Symbolic Model Checking, the paper that defines the language
Kind 2 user documentation, for the engines and the options kMoXI shares with Kind 2

People

kMoXI is developed by the Kind 2 team at The University of Iowa.