KIND-INV
KIND-INV generates in an automatic fashion Boolean and Integer type invariants for Lustre programs.
The tool produces quantifier-free k-inductive invariants for a given Lustre program. KIND-INV relies on SMT solvers and capitalizes on their ability to quickly generate counter-models of non-invariant conjectures.
We have carried extensive experiments with a large set of Lustre programs and associated safety properties. The invariants generated with KIND-INV considerably increase the number of provable safety properties; moreover, they do not slow down the processing of properties already provable without invariants.