View on GitHub

Kind 2

Multi-engine SMT-based automatic model checker for safety properties of Lustre programs

About

Kind 2 is an open-source, multi-engine, SMT-based automatic model checker for safety properties of Lustre programs. It takes as input a Lustre file annotated with properties to prove invariant, and outputs for each property either a confirmation or a counterexample, 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

Download

Documentation

Try Kind 2 Online

Visit our web interface to try Kind 2 from your browser.

Contact

Cesare Tinelli

People

Formerly: