文章基本信息

标题：PKind: A parallel k-induction based model checker
本地全文：下载
作者：Temesghen Kahsai ; Cesare Tinelli
期刊名称：Electronic Proceedings in Theoretical Computer Science
电子版ISSN：2075-2180
出版年度：2011
卷号：72
页码：55-62
DOI：10.4204/EPTCS.72.6
出版社：Open Publishing Association
摘要：PKind is a novel parallel k-induction-based model checker of invariant properties for finite- or infinite-state Lustre programs. Its architecture, which is strictly message-based, is designed to minimize synchronization delays and easily accommodate the incorporation of incremental invariant generators to enhance basic k-induction. We describe PKind's functionality and main features, and present experimental evidence that PKind significantly speeds up the verification of safety properties and, due to incremental invariant generation, also considerably increases the number of provable ones.