Kind 2 is an open-source, multi-engine, SMT-based automatic model checker for safety properties of Lustre programs. It takes as input a Lustre file annotated with properties to prove invariant, and outputs for each property either a confirmation or a counterexample, a sequence inputs that falsifies the property. Kind 2 is a from-scratch reimplementation of the Kind model checker.
Keywords for this software
References in zbMATH (referenced in 3 articles )
Showing results 1 to 3 of 3.
- Champion, Adrien; Chiba, Tomoya; Kobayashi, Naoki; Sato, Ryosuke: ICE-based refinement type discovery for higher-order functional programs (2020)
- Qin, Xudong; Bliudze, Simon; Madelaine, Eric; Hou, Zechen; Deng, Yuxin; Zhang, Min: SMT-based generation of symbolic automata (2020)
- Cimatti, Alessandro; Griggio, Alberto; Mover, Sergio; Tonetta, Stefano: Infinite-state invariant checking with IC3 and predicate abstraction (2016)