Dear all,
We are happy to announce the new official release (v1.0.1) of Kind 2,
an open-source, multi-engine, SMT-based automatic model checker for
safety properties of Lustre programs [1].
This version adds features that considerably improve performance and
provide new functionality. These include:
- a new assume/guarantee-based contract language extending Lustre
- contract-driven modular and compositional verification
- a significantly improved auxiliary invariant generation engine
- compilation of Lustre models to Rust
- test-case generation
- proof-certificate generation
- various performance improvements and bug fixes
Please refer to the CHANGES document [2] for a more detailed
description, and to the user's documentation [3] of these new
features.
The latest version of Kind 2 can be downloaded from
https://github.com/kind2-mc/kind2/releases and is distributed in
source form, as well as binaries for both Linux and Mac OS X.
Feedback and feature requests are most welcome. Please contact the
developers or open an issue directly on Github at
https://github.com/kind2-mc/kind2/issues/new
If you want to participate in discussions with developers and other
users of Kind 2, you are encouraged to join the kind2-users group at
https://groups.google.com/d/forum/kind2-users
Best,
The Kind 2 Development Team
[1]
http://kind.cs.uiowa.edu
[2]
https://github.com/kind2-mc/kind2/tree/v1.0.0/CHANGES.md
[3]
https://github.com/kind2-mc/kind2/tree/v1.0.0/doc/usr/content