Journal article
PKIND: A parallel k-induction based model checker
Electronic proceedings in theoretical computer science, Vol.72(72), pp.55-62
11/01/2011
DOI: 10.4204/EPTCS.72.6
Abstract
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.
Details
- Title: Subtitle
- PKIND: A parallel k-induction based model checker
- Creators
- Temesghen Kahsai - University of IowaCesare Tinelli - University of Iowa
- Resource Type
- Journal article
- Publication Details
- Electronic proceedings in theoretical computer science, Vol.72(72), pp.55-62
- DOI
- 10.4204/EPTCS.72.6
- ISSN
- 2075-2180
- eISSN
- 2075-2180
- Publisher
- Open Publ Assoc
- Number of pages
- 8
- Grant note
- 1049674 / NSF; National Science Foundation (NSF) FA9550-09-1-0517 / AFOSR; United States Department of Defense; Air Force Office of Scientific Research (AFOSR)
- Language
- English
- Date published
- 11/01/2011
- Academic Unit
- Computer Science
- Record Identifier
- 9984411089902771
Metrics
7 Record Views