The JKind model checker

Andrew Gacek, John Backes, Mike Whalen, Lucas Wagner, Elaheh Ghassabani

Research output: Chapter in Book/Report/Conference proceedingConference contribution

33 Scopus citations

Abstract

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 languageEnglish (US)
Title of host publicationComputer Aided Verification - 30th International Conference, CAV 2018, Held as Part of the Federated Logic Conference, FloC 2018, Proceedings
EditorsGeorg Weissenbacher, Hana Chockler
PublisherSpringer- Verlag
Pages20-27
Number of pages8
ISBN (Print)9783319961415
DOIs
StatePublished - Jan 1 2018
Event30th International Conference on Computer Aided Verification, CAV 2018 Held as Part of the Federated Logic Conference, FloC 2018 - Oxford, United Kingdom
Duration: Jul 14 2018Jul 17 2018

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume10982 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference30th International Conference on Computer Aided Verification, CAV 2018 Held as Part of the Federated Logic Conference, FloC 2018
Country/TerritoryUnited Kingdom
CityOxford
Period7/14/187/17/18

Bibliographical note

Funding Information:
Acknowledgments. The work presented here was sponsored by DARPA as part of the HACMS program under contract FA8750-12-9-0179.

Publisher Copyright:
© The Author(s) 2018.

Fingerprint

Dive into the research topics of 'The JKind model checker'. Together they form a unique fingerprint.

Cite this