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

Application domain/field

• Model checker
• Synchronous systems

Type of tool

Model checker

Expected input

• Model
• Properties to be checked

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.