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...
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 |
Similar Items
-
Extending SMTCoq, a Certified Checker for SMT (Extended Abstract)
by: Burak Ekici, et al.
Published: (2016-06-01) -
CoInDiVinE: Parallel Distributed Model Checker for Component-Based Systems
by: Nikola Beneš, et al.
Published: (2011-10-01) -
Hierarchical State Machines as Modular Horn Clauses
by: Pierre-Loïc Garoche, et al.
Published: (2016-07-01) -
Synthesizing Modular Invariants for Synchronous Code
by: Pierre-Loic Garoche, et al.
Published: (2014-12-01) -
Principles of the spin model checker /
by: 288973 Ben-Ari, Mordechai
Published: (2008)