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

  • 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 [Lustre Files]
      * pkind with invariant generation: > pkind -with-inv-gen [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 [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