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]

      In order to use the font end, "bin/pkind-main" has to be in the system path. Hence, use "make" and then "make install". If you prefer not use the front end you can directly use bin/pkind-main, i.e.

      * 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.
counter for vBulletin