JKind is a tool 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 Rockwell Collins including the AGREE tool and the SIMPAL tool. JKind is designed to be cross-platform, reliable, and easy to extend, with power and performance as secondary goals. JKind is mostly compatible with the KIND and Kind 2 model checkers.
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 is primarily developed by Andrew Gacek.