PKind: A parallel k-induction based model checker

TL;DR

PKind is a parallel, message-based model checker for Lustre programs that accelerates safety property verification and improves invariant proof capabilities through incremental invariant generation.

Contribution

It introduces a novel parallel k-induction architecture that minimizes synchronization delays and integrates incremental invariant generators for enhanced verification.

Findings

Significantly speeds up safety property verification

Increases the number of provable invariants

Efficiently handles finite and infinite-state Lustre programs

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.