The Kind 2 Model Checker
The Kind 2 Model Checker
复制标题
DOI：
10.1007/978-3-319-41540-6_29
复制
发表时间：
2016-07
期刊：
影响因子：
--
通讯作者：
A. Champion;Alain Mebsout;Christoph Sticksel;C. Tinelli
中科院分区：
文献类型：
--
作者：
A. Champion;Alain Mebsout;Christoph Sticksel;C. Tinelli
Kind2是一个开源、多引擎、基于SMT的模型检查器，用于有限状态和无限状态同步反应系统的安全属性。它接受用Lustre语言的扩展编写的模型作为输入，该扩展允许指定系统组件的假定-保证样式的合同。Kind2是基于其前身PKindModel检查器使用的技术从头开始实现的。本文讨论了在不变量生成方面对PKIND的一些改进。它还介绍了两个主要功能：基于合同的组合推理和证书生成。
Kind2 is an open-source, multi-engine, SMT-based model checker for safety properties of finite- and infinite-state synchronous reactive systems. It takes as input models written in an extension of the Lustre language that allows the specification of assume-guarantee-style contracts for system components.Kind2 was implemented from scratch based on techniques used by its predecessor, thePKindmodel checker. This paper discusses a number of improvements overPKindin terms of invariant generation. It also introduces two main features: contract-based compositional reasoning and certificate generation.