Announcing Kind 2 v0.8.0
15 views
Skip to first unread message
Christoph Sticksel
Jun 9, 2015, 3:34:41 PM6/9/15
to kind2-a...@googlegroups.com, kind2...@googlegroups.com
Dear all,
We are happy to announce the official release of Kind 2 v0.8.0,
an open-source, multi-engine, SMT-based automatic model checker for
safety properties of Lustre programs.
Kind 2 is a from-scratch reimplementation of the Kind model checker.
It runs under Linux and Mac OS X and is available both in binary and
source form from http://kind.cs.uiowa.edu . You can try Kind 2 online at
http://kind.cs.uiowa.edu:8080/kind .
Kind 2 takes as input a Lustre file annotated with properties to
prove invariant, and outputs which of the properties are invariants and
which are not. For each non-invariant property it also provides
a counterexample as a sequence of inputs that falsifies the
property. Information about each property is output incrementally as it
is discovered. To ease processing by client tools, Kind 2 can output
its results in XML format.
This version adds features that improve performance as well as provide
new functionality. See CHANGES and the manual for more details.
This release is an intermediate release, and the next release will
include strategies for contract-based compositional verification,
support for arrays, and other features currently under development.
Feedback and feature requests are most welcome. Either contact the
developers, or open an issue directly on Github
at https://github.com/kind2-mc/kind2/issues/new
If you would like to receive announcements of future releases, please
accept our invitation to the kind2-announce group on Google. If you want
to participate in discussions with developers and other users, also
consider joining the kind2-users group
at https://groups.google.com/d/forum/kind2-users
Best,
The Kind 2 Development Team
Cesare Tinelli
Adrien Champion
Alain Mebsout
Christoph Sticksel
We are happy to announce the official release of Kind 2 v0.8.0,
an open-source, multi-engine, SMT-based automatic model checker for
safety properties of Lustre programs.
Kind 2 is a from-scratch reimplementation of the Kind model checker.
It runs under Linux and Mac OS X and is available both in binary and
source form from http://kind.cs.uiowa.edu . You can try Kind 2 online at
http://kind.cs.uiowa.edu:8080/kind .
Kind 2 takes as input a Lustre file annotated with properties to
prove invariant, and outputs which of the properties are invariants and
which are not. For each non-invariant property it also provides
a counterexample as a sequence of inputs that falsifies the
property. Information about each property is output incrementally as it
is discovered. To ease processing by client tools, Kind 2 can output
its results in XML format.
This version adds features that improve performance as well as provide
new functionality. See CHANGES and the manual for more details.
This release is an intermediate release, and the next release will
include strategies for contract-based compositional verification,
support for arrays, and other features currently under development.
Feedback and feature requests are most welcome. Either contact the
developers, or open an issue directly on Github
at https://github.com/kind2-mc/kind2/issues/new
If you would like to receive announcements of future releases, please
accept our invitation to the kind2-announce group on Google. If you want
to participate in discussions with developers and other users, also
consider joining the kind2-users group
at https://groups.google.com/d/forum/kind2-users
Best,
The Kind 2 Development Team
Cesare Tinelli
Adrien Champion
Alain Mebsout
Christoph Sticksel
Reply all
Reply to author
Forward
0 new messages