Table of Contents

Getting Started

• Kind 2
  • Try Kind 2 Online
  • Download
  • Required Software
  • VS Code Extension
  • Docker
  • Building and installing
  • Development
  • Documentation

Techniques

• Techniques
  • Compositional reasoning
  • Modular reasoning
  • Refinement in compositional and modular analyses
• k-Induction
  • Options
• Invariant Generation
  • Options
  • Lock Step K-induction
• IC3
  • IC3-IA Options
  • IC3-QE Options

Inputs and Outputs

• Kind 2 Input
  • Properties and top-level node
  • Contracts
  • Partially defined nodes
  • The imported keyword
  • Functions
  • If statements and frame conditions
  • Nondeterministic choice operator
  • Polymorphic nodes
• Arrays
  • Lustre arrays
  • Extension to unbounded arrays
• Machine Integers
  • Declarations
  • Values
  • Semantics
  • Operations
  • Limitations
• Refinement Types
  • Declarations
  • Semantics
  • Operations
  • Realizability
  • Restrictions
• Enumeration types
  • N-way merge
• History Types
• Abstract Types
• JSON / XML Output
  • JSON format
  • XML format
• Exit codes
  • Code Convention
  • Former Convention

Advanced Features

• Contract Semantics
  • Assume-guarantee contracts
  • Modes
• Post Analysis Treatments
  • Prerequisites
• Test Generation
  • Combinations of modes as abstractions
  • Generating test cases
  • Oracle generation
  • An example of a Test Execution Engine
• Compilation to Rust
  • Technical details
  • Assertions, properties and contracts
• Proof Certificates
  • Certification chain
  • Producing certificates and proofs with Kind 2
  • Contents of certificates
  • LFSC signature
• Contract Generation
• Invariant Printing
• Interpreter
  • Structure of the input file
  • Integers and reals
  • Records
  • Arrays
  • Tuples
• Inductive Validity Core
  • Options
  • Example
  • Minimizing over a subset of the assumptions/guarantees
  • Computing all Inductive Validity Cores
• Minimal Cut Set
  • Options
  • Example
• Contract Check
• Assumption Generation

License

• Apache License