PKind: A parallel k-induction based model checker

Details PKind: A parallel k-induction based model checker PKind: A parallel k-induction based model checker

2011-11-02

arxiv.org/abs/1111.0372v1

EPTCS 72, 2011, pp. 55-62

Computer Science

Logic in Computer Science

In Proceedings PDMC 2011, arXiv:1111.0064

Scientific paper

10.4204/EPTCS.72.6

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.

Affiliated with

Also associated with

No associations

Rating

PKind: A parallel k-induction based model checker does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.

If you have personal experience with PKind: A parallel k-induction based model checker, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and PKind: A parallel k-induction based model checker will most certainly appreciate the feedback.

Rate now

Comments { 0 }

Profile ID: LFWR-SCP-O-327457