PV4 ⊧ JKindinfers invariants and checks user-specified properties for a Lustre system
- Model checker
- Synchronous systems
Type of toolModel checker
- Properties to be checked
Format:.lus file (Lustre language)
Expected outputA list of valid properties and invalid properties, including the time it took to verify/falsify each property.
InternalsSMT-based infinite-state model checker for safety properties. Models and properties are specified in Lustre. The JKind architecture consists of 5 separate 'engines':
- Bounded Model Checking (BMC) engine for standard iterative unrolling to find counterexamples.
- k-Induction engine to perform the inductive step of k-induction
- Invariant generation engine that generates invariants based on templates.
- Property Directed Reachability (PDR) engine to do property directed reachability.
- Advice engine to generate invariants based on previous JKind runs.