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 portable, easy to install, performance competitive with other state-of-the-art model checkers, and has features designed to improve the results presented to users: inductive validity cores for proofs and counterexample smoothing for test-case generation. It serves as the back-end for various industrial applications.
|Original language||English (US)|
|Title of host publication||Computer Aided Verification - 30th International Conference, CAV 2018, Held as Part of the Federated Logic Conference, FloC 2018, Proceedings|
|Editors||Georg Weissenbacher, Hana Chockler|
|Number of pages||8|
|State||Published - Jan 1 2018|
|Event||30th International Conference on Computer Aided Verification, CAV 2018 Held as Part of the Federated Logic Conference, FloC 2018 - Oxford, United Kingdom|
Duration: Jul 14 2018 → Jul 17 2018
|Name||Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)|
|Conference||30th International Conference on Computer Aided Verification, CAV 2018 Held as Part of the Federated Logic Conference, FloC 2018|
|Period||7/14/18 → 7/17/18|
Bibliographical noteFunding Information:
Acknowledgments. The work presented here was sponsored by DARPA as part of the HACMS program under contract FA8750-12-9-0179.