Note:
This system is no longer under active development.
Please check its successor Kind 2.
About
KIND is an automatic verification tool for safety properties of Lustre programs.
KIND's main features:
- Inductive or BMC mode.
- Abstraction/Refinement techniques.
- Support for CVC3 and Yices
- Automatic invariant generation
- Efficient parallel implementation of the k-induction procedure with incremental invariant generation.
- Incremental verification of multiple properties.
- .. for a complete lists of options you can look in here.
News
- 14.06.2014 : The successor of Kind, Kind 2, has been officially released.
- 10.29.2013 : Updated the website with new papers, Kind version 1.8.6b and experimental results of various papers.
- 09.23.2012: Kind version 1.8.4 has been released. Release Notes:
- Added a standalone tool Kind-Test-Gen: A BMC multi-properties verification tool.
- Invariant generation based on abstract interpretation (Note. Kind-AI need to be compiled separately).
- Resolved a few bugs.
- 01.26.2012:"Incremental verification with mode variable invariants in state machines" paper has been accepted at NASA Formal Methods 2012.
- 01.16.2012: KIND version 1.8 has been released. Release Notes:
- Fixed a bug in the multiple property verification.
- Added a front end for pkind. With this front end there is no need to call the MPI primitives such as mpiexec.
- pkind without invariant generation: pkind options [Lustre Files]
- pkind with invariant generation: pkind -with-inv-gen options [Lustre Files]
* mpiexec -np [2 or 3] pkind-main options [LUSTRE FILE]
- Added an option for a clean verbose mode.
- 12.12.2011: KIND version 1.7.4 has been released. Release Notes:
- Resolved some internal bugs.
- 12.04.2011: KIND version 1.7.3 has been released. Release Notes:
- Added an option "-no_multi" to do non-incremental verification of multiple properties
- Resolved some internal bugs.
- 11.21.2011: KIND version 1.7.2 has been released. Release Notes:
- An option to generate results in XML format.
- Resolved some internal bugs.
- 10.12.2011: KIND version 1.7 has been released. Release Notes:
- A much cleaner installation process using an auto configuration script.
- This version can generate invariants between mode variables. The user has to explicitly declare the variables of type mode. For example, if variables x and y ranges over [1..5] and [10..18] respectively, in the lustre program those has to be declared as x: subrange [1,5] of int; y: subrange [10,18] of int.
- 09.01.2011: KIND Version 1.6 has been released. Release Notes:
- Option to verify multiple properties in an incremental fashion.
- Option to print inductive counterexamples.
- 06.20.2011: "PKind: A parallel k-induction based model checker" paper has been accepted at PDMC 2011.
- 05.12.2011: KIND Version 1.5 has been released.
- 02.08.2011: Parallel Kind has been released.
- 02.07.2011: "Instantiation-based invariant discovery" paper has been accepted.
- 12.06.2010: KIND has a new website.