Announcing Kind 2 3.0.0

[kind2-announce]

Dear all,

We are happy to announce the new official release (v3.0.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:

- New map and set types.
- Support for structural equality for arrays, maps, and sets.
- Bottom-up type inference for polymorphic node and function calls (using base types only).
- New syntax for specifying contracts.
- New type ascription operator.
- New conditional expression and blocks with lazy semantics, and short-circuiting versions of 'and', 'or', and '=>'.
- Support for machine integers of arbitrary concrete size, including generation of invariant candidates.
- New built-in operator `choose`. Like `any`, it denotes an arbitrary stream of values, but the value is determined by the free variables in the predicate, effectively behaving like a function of those variables.
- Support for subranges with symbolic constant bounds.
- Support for quantifiers in refinement type predicates.
- Support for a concise refinement type syntax for quantified variables (e.g. `forall (i: int | i > 0)`).
- New safety proof production feature based on the new cvc5 CPC proof format (replaces LFSC); compatible with cvc5 1.3.2.
- Support for Bitwuzla as an interpolating solver.
- New contract monitor feature to check a given trace satisfies a contract.
- Verification of constant definitions and realizability checks of free constants (a.k.a system parameters) with refinement types.

Please refer to the CHANGES document [2] for a more detailed
description and a list of breaking changes, and to
the user documentation [3] for further 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.
It can also be installed through OPAM.

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/v3.0.0/CHANGES.md
[3] https://kind.cs.uiowa.edu/kind2_user_doc/