Kind is a k-induction based verifier for safety properties in Lustre.
| [HT08] | George Hagen and Cesare Tinelli. Scaling up the formal verification of Lustre programs with SMT-based techniques. In Proceedings of the 8th International Conference on Formal Methods in Computer-Aided Design (FMCAD'08), Portland, Oregon. IEEE, 2008. [ Preprint | BibTeX ] |
| [H08] | George Hagen. Verifying safety properties of Lustre programs: an SMT-based approach. PhD dissertation. Department of Computer Science. The University of Iowa. December 2008. [ Dissertation | BibTeX ] |
The most recent version of Kind is distributed as a tarball with both source files (mostly in OCaml) and executables for Linux and Mac OS 10.4. To compile the sources, you will need these files, as well as:
In addition, you will need a compatible SMT solver. Currently Kind supports Yices and CVC3:
Currently the most stable and efficient version utilizes a wrapper version of Yices that needs to be compiled (see the included INSTALL file for instructions).
Available versions:
The Lustre benchmarks mentioned in [HT08] can be found here (gzipped tar file)
Experiment results can be found here (gzipped Excel spreadsheet)
Kind was developed by George Hagen (main developer) and Cesare Tinelli.
If you have any questions, comments, suggestions or complaints about Kind please contact Cesare Tinelli.