PKind: A parallel k-induction based model checker

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.

In Proceedings PDMC 2011, arXiv:1111.0064

References in corpus (1)

• Tarmo: A Framework for Parallelized Bounded Model Checking

Cited by in corpus (10)

• Combining k-Induction with Continuously-Refined Invariants
• Hierarchical State Machines as Modular Horn Clauses
• Model Counting Modulo Theories
• Software Verification with PDR: Implementation and Empirical Evaluation of the State of the Art
• Generating Property-Directed Potential Invariants By Backward Analysis
• Invariant stream generators using automatic abstract transformers based on a decidable logic
• IC3 Modulo Theories via Implicit Predicate Abstraction
• Model Checking Embedded C Software using k-Induction and Invariants (extended version)
• Model Checking C Programs with Loops via k-Induction and Invariants
• "ReLIC: Reduced Logic Inference for Composition" for Quantifier Elimination based Compositional Reasoning and Verification