JKind

An infinite-state model checker for safety properties

JKind is an infinite state model checker for verifying safety properties of synchronous systems. Systems and their properties are expressed in the Lustre language. Verification is based on k-induction and property directed reachability using a back-end SMT solver. A verified property is guaranteed to be true for all runs of the system. A falsified property is reported with an explicit counterexample demonstrating the property violation.

JKind is used as the back-end model checker for many projects and tools at Collins Aerospace, including AGREE, SpeAR, and SIMPAL. JKind is also used for internal projects releated to test case generation and certification.

JKind requires at least Java 8. JKind uses SMTInterpol by default (packaged with JKind), but it also supports Z3, Yices 1, Yices 2, CVC4, and MathSAT.

JKind Xtext is an Eclipse plug-in with syntax highlighting and static analysis for Lustre code. It also runs JKind and reports the results graphically.

JKind was primarily developed by Andrew Gacek and is maintained by Loonwerks.

Publications