The JKind Model Checker

A. Gacek, J. Backes, M. Whalen, L. Wagner, E. Ghassabani

(Submitted December 2017)

JKind is an open-source industrial model checker developed by Rockwell Collins and the University of Minnesota. JKind uses multiple parallel engines to prove or falsify safety properties of infinite state models. It is performance competitive with other state-of-the-art model checkers and serves as the back-end for various industrial applications.