PKind: A parallel k-induction based model checker

PKind: A parallel k-induction based model checker

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 generat...

Full description

Bibliographic Details
Main Authors: Temesghen Kahsai, Cesare Tinelli
Format: Article
Language:English
Published: Open Publishing Association 2011-10-01
Series:Electronic Proceedings in Theoretical Computer Science
Online Access:http://arxiv.org/pdf/1111.0372v1
id doaj-64381d246e4747c2a427ee97cb86c3bd
record_format Article
spelling doaj-64381d246e4747c2a427ee97cb86c3bd2020-11-24T23:42:21ZengOpen Publishing AssociationElectronic Proceedings in Theoretical Computer Science2075-21802011-10-0172Proc. PDMC 2011556210.4204/EPTCS.72.6PKind: A parallel k-induction based model checkerTemesghen KahsaiCesare TinelliPKind 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.http://arxiv.org/pdf/1111.0372v1
collection DOAJ
language English
format Article
sources DOAJ
author Temesghen Kahsai
Cesare Tinelli
spellingShingle Temesghen Kahsai
Cesare Tinelli
PKind: A parallel k-induction based model checker
Electronic Proceedings in Theoretical Computer Science
author_facet Temesghen Kahsai
Cesare Tinelli
author_sort Temesghen Kahsai
title PKind: A parallel k-induction based model checker
title_short PKind: A parallel k-induction based model checker
title_full PKind: A parallel k-induction based model checker
title_fullStr PKind: A parallel k-induction based model checker
title_full_unstemmed PKind: A parallel k-induction based model checker
title_sort pkind: a parallel k-induction based model checker
publisher Open Publishing Association
series Electronic Proceedings in Theoretical Computer Science
issn 2075-2180
publishDate 2011-10-01
description 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.
url http://arxiv.org/pdf/1111.0372v1
work_keys_str_mv AT temesghenkahsai pkindaparallelkinductionbasedmodelchecker
AT cesaretinelli pkindaparallelkinductionbasedmodelchecker
_version_ 1725504837414551552

Similar Items