JKind swMATH ID: 21029 Software Authors: Andrew Gacek Description: JKind is an SMT-based infinite-state model checker for safety properties in Lustre. JKind uses parallel cooperating engines including k-induction, property directed reachability, and template-based invariant generation. Downloads: JKind is written in Java and requires at least Java 8. The latest release of JKind is available on the releases page. This includes the JKind model checker as well as the JRealizability, JLustre2Excel, and JLustre2Kind tools. Design Goals: JKind is designed to be cross-platform, reliable, and easy to extend. Power and performance are secondary goals. Additionally, JKind attempts to be mostly compatible with pkind and Kind 2, though this varies over time due to developments in both systems. Alternative Solvers (optional): By default, JKind is packaged with SMTInterpol as its underlying SMT solver. Advanced users may wish to install alternative solvers such as Z3, Yices (version 1), Yices 2, CVC4, or MathSAT. Homepage: https://github.com/agacek/jkind/ Source Code: https://github.com/agacek/jkind/ Related Software: Kind 2; Paracooba; Kissat; CaDiCaL; AIGER; ABC; MiniSat; nuXmv; CTIGAR; GitHub; Tip; PKind; InvGen; MathSAT5; PVS Cited in: 2 Publications all top 5 Cited by 7 Authors 1 Biere, Armin 1 Cimatti, Alessandro 1 Griggio, Alberto 1 Heljanko, Keijo 1 Mover, Sergio 1 Tonetta, Stefano 1 Yu, Emily Cited in 1 Serial 1 Formal Methods in System Design Cited in 1 Field 2 Computer science (68-XX) Citations by Year