Kind 2

介紹

Multi-engine SMT-based automatic model checker for safety properties of Lustre programs

翻譯準備中

取自儲存庫 README

README

正在載入完整 README。 以下為已儲存的摘錄。

Kind 2 is a multi-engine, parallel, SMT-based automatic model checker for safety properties of Lustre programs. Kind 2 is a command-line tool. It takes as input a Lustre file annotated with properties to be proven invariant (see Kind 2 Input), and outputs which of the properties are true for all inputs, as well as an input sequence for those properties that are falsified. To ease processing by external tools, Kind 2 can output its results in JSON and XML formats (see JSON / XML Output).