PV4 JKindinfers invariants and checks user-specified properties for a Lustre system

Application domain/field

Type of tool

Model checker

Expected input

Format:

.lus file (Lustre language)

Expected output

A list of valid properties and invalid properties, including the time it took to verify/falsify each property.

Internals

SMT-based infinite-state model checker for safety properties. Models and properties are specified in Lustre. The JKind architecture consists of 5 separate 'engines':
  1. Bounded Model Checking (BMC) engine for standard iterative unrolling to find counterexamples.
  2. k-Induction engine to perform the inductive step of k-induction
  3. Invariant generation engine that generates invariants based on templates.
  4. Property Directed Reachability (PDR) engine to do property directed reachability.
  5. Advice engine to generate invariants based on previous JKind runs.
Uses SMTInterpol as an SMT-solver to prove/falsify properties.

Comments

There exists an Eclipse plug-in with syntax highlighting and static analysis for Lustre code which also runs JKind and reports the results graphically.
Lustre

Links

Related papers

The JKind Model Checker

Last publication date

18 July 2018

Related tools

ProVerB specific



ProVerB is a part of SLEBoK. Last updated: February 2023.