kind2:基于多引擎SMT的自动模型检查器，可确保Lustre程序的安全性-源码

种类2 是基于Lustre程序安全性的多引擎，基于SMT的并行并行自动模型检查器。 种类2是命令行工具。 它以注有被证明为不变的属性的Lustre文件作为输入（请参见 ），并输出所有输入中正确的属性，以及伪造的那些属性的输入序列。 为了简化外部工具的处理，种类2可以将结果以JSON和XML格式 （请参阅 ）。 默认情况下，种类2运行用于边界模型检查（BMC）的过程，用于k归纳的两个过程（一个用于k = 2的固定值，另一个用于增加k的值），几个用于不变生成的过程以及一个过程同时对所有属性的IC3进行并行处理。 它以增量方式将反例输出到属性以及经证明是不变的属性。 以下命令行选项控制其操作（运行kind2 --help可获得完整列表）。 见用于配置实例和每种技术的更多细节。 --enable {BMC|IND|IND2|IC3|INVGEN|INVGENOS|...}选择模型检查引擎