View on GitHub

Kind 2

Multi-engine SMT-based automatic model checker for synchronous reactive systems

About

Kind 2 is an open-source, multi-engine, SMT-based automatic model checker for safety properties of finite-state or infinite-state synchronous reactive systems expressed as in an extension of the Lustre language. In its basic configuration it takes as input one or more Lustre files annotated with properties to be proven invariant, and outputs for each property either a confirmation or a counterexample, i.e., a sequence inputs that falsifies the property. More advanced features include contract-based compositional verification, proof generation for proven properties, and contract-based test generation.

Kind 2 is a from-scratch reimplementation of the Kind model checker.

Main features

Mailing Lists

kind2-announce@googlegroups.com
Release announcements
kind2-users@googlegroups.com
Discussions between users and developers

Documentation

Try Kind 2 Online

Visit our web interface to try Kind 2 from your browser

Download

Executables

VS Code Extension

You can also install our extension for VS Code which provides support for Kind 2. The extension contains Linux and macOS binaries for Kind 2 and Z3 ready to use. Windows is also supported through WSL2 (see here for more details).

Docker

Kind 2 is also available on Docker Hub. Follow these steps to install one of the images.

People

Current

Alumni

Other contributors to the Kind 2 codebase can be found here.

Publications

Daniel Larraz, Cesare Tinelli. Finding Locally Smallest Cut Sets using Max-SMT. In ACM SIGAda Ada Letters, 2022.

Daniel Larraz, Arjun Viswanathan, Mickaël Laurent, Cesare Tinelli. Beyond model checking of idealized Lustre in Kind 2. In ACM SIGAda Ada Letters, 2022.

Daniel Larraz, Cesare Tinelli. Realizability Checking of Contracts with Kind 2. CoRR abs/2205.09082, 2022.

Daniel Larraz, Mickaël Laurent, Cesare Tinelli. Merit and Blame Assignment with Kind 2. In Proceedings of the 26th International Conference on Formal Methods for Industrial Critical Systems (FMICS), 2021.

Lucas Wagner, Alain Mebsout, Cesare Tinelli, Darren Cofer, Konrad Slind. Qualification of a Model Checker for Avionics Software Verification. In Proceedings of the 9th NASA Formal Methods Symposium (NFM), 2017.

Alain Mebsout, Cesare Tinelli. Proof Certificates for SMT-based Model Checkers for Infinite-state Systems. In Proceedings of 16th Conference on Formal Methods in Computer-Aided Design (FMCAD), 2016.

Adrien Champion, Alain Mebsout, Christoph Sticksel, Cesare Tinelli. The Kind 2 Model-Checker. In Proceedings of 28th International Conference on Computer Aided Verification (CAV), 2016.

Adrien Champion, Arie Gurfinkel, Temesghen Kahsai, Cesare Tinelli. CoCoSpec: A Mode-Aware Contract Language for Reactive Systems. In Proceedings of the 14th International Conference on Software Engineering and Formal Methods (SEFM), 2016.

Pierre-Loïc Garoche, Temesghen Kahsai, Cesare Tinelli. Incremental Invariant Generation using Logic-based Automatic Abstract Transformers. In Proceedings of the 5th NASA Formal Methods Symposium (NFM), 2013.

Temesghen Kahsai, Pierre-Loïc Garoche, Cesare Tinelli, Mike Whalen. Incremental verification with mode variable invariants in state machines. In Proceedings of the 4th NASA Formal Methods Symposium (NFM), 2012.

Temesghen Kahsai, Cesare Tinelli. PKind: A parallel k-induction based model checker. In Proceedings of 10th International Workshop on Parallel and Distributed Methods in verifiCation (PDMC), 2011.

Temesghen Kahsai, Yeting Ge, Cesare Tinelli. Instantiation-Based Invariant Discovery. In Proceedings of the 3rd NASA Formal Methods Symposium (NFM), 2011.

George Hagen, Cesare Tinelli. Scaling up the formal verification of Lustre programs with SMT-based techniques. In Proceedings of the 8th International Conference on Formal Methods in Computer-Aided Design (FMCAD), 2008.

George Hagen. Verifying safety properties of Lustre programs: an SMT-based approach. PhD dissertation. Department of Computer Science. The University of Iowa. December 2008.

Acknowledgments

The Kind logo was designed by Daniel Yahyazadeh.

The development of Kind 2 has been partially supported with funding from the following organizations.