期刊
COMPUTER AIDED VERIFICATION: 28TH INTERNATIONAL CONFERENCE, CAV 2016, PT II
卷 9780, 期 -, 页码 510-517出版社
SPRINGER INTERNATIONAL PUBLISHING AG
DOI: 10.1007/978-3-319-41540-6_29
关键词
-
Kind 2 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. Kind 2 was implemented from scratch based on techniques used by its predecessor, the PKind model checker. This paper discusses a number of improvements over PKind in terms of invariant generation. It also introduces two main features: contract-based compositional reasoning and certificate generation.
作者
我是这篇论文的作者
点击您的名字以认领此论文并将其添加到您的个人资料中。
推荐
暂无数据