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 synchronous reactive systems expressed as in an extension of the Lustre language. 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.

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

People

Formerly: