Announcing Kind 2 1.3.0

[kind2-announce]

Dear all,

We are happy to announce the new official release (v1.3.0) of Kind 2, 

an open-source, multi-engine, SMT-based automatic model checker for 

safety properties of Lustre programs [1]. 

In addition to several improvements and bug fixes, this release includes

the following new functionalities:

- Computation of Inductive Validity Cores and Minimal Cut Sets.

- Invariant generation for machine integers.

- IC3 model checking engine for machine integers.

- Support for abstract types (thanks to Amos Robinson).

- Support for SMT solvers Boolector and MathSAT.

- A new command-line option to only parse Lustre inputs.

Please refer to the CHANGES document [2] for a more detailed 

description, and to the user's documentation [3] for more details.

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 macOS. 

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/blob/v1.3.0/CHANGES.md

[3] https://kind.cs.uiowa.edu/kind2_user_doc/