package kind2

  1. Overview
  2. Docs
Multi-engine, parallel, SMT-based automatic model checker for safety properties of Lustre programs

Install

Dune Dependency

Authors

Maintainers

Sources

v1.5.1.tar.gz
md5=925a61376d7b9d27945e9407e228c7e0
sha512=04dd7dfa2683ab8517c150a0bfcbc168e2668399dc641cdc87ea39fb901985146db16b11b1551b02bf60b33a5c332794187a04ef5d6126ca72831eee524a1ebb

CHANGES.md.html

Kind 2 v1.5.1

This release includes performance improvements and various fixes. Notably:

  • Improve performance of realizability checks with Z3.

  • Fix realizability check of imported functions.

  • Fix realizability check when --ae_val_use_ctx is false (bug introduced in v1.5.0).

  • Fix generation of tracing information when a contract is proven unrealizable.

  • Fix shape of generated invariant candidates when --invgen_all_out is true.

  • Fix generation of SMT-LIB 2 certificates.

  • Make Kind 2 compatible with the latest version (5.1.4) of the OCaml bindings for ZMQ.

In addition, this version adds support for a new Visual Studio Code extension for Kind 2.

Thanks to Andreas Katis for his feedback and bug reports.

Kind 2 v1.5.0

New features:

  • Print a deadlocking trace and a set of conflicting constraints when a contract is proven unrealizable.

  • Multiple nodes can be annotated as main nodes so that analysis results for common subnodes are shared in modular analysis.

  • New option to dump each counterexample to a file (--dump_cex).

Improvements:

  • Require and ensure clauses of contract modes are eligible elements for IVCs and MCSs when the contracts category is selected.

  • Print values of (free) constants in counterexamples.

  • Print summary before terminating when CTRL-C is pressed.

  • Prevent invariant generation engine from crashing when processing global constants.

  • Fix handling of XOR operator in IC3.

  • Fix minor issues in IVC/MCS module.

  • Other bug fixes and enhancements.

Changes:

  • Kind 2 now requires:

    • OCaml 4.09 or later

    • Dune 2.7 or later

Thanks to M. Anthony Aiello, Andreas Katis, and Amos Robinson for their feedback and suggestions.

Kind 2 v1.4.0

New features:

  • New option for checking contracts of imported nodes (see documentation).

    • Current checks: realizability and satisfiability checking.

Improvements:

  • Improve compositional reasoning about assumptions of called nodes.

    • See issue #736 for more details (thanks to Amos Robinson).

  • Print values of ghost variables in counterexamples.

  • Fix and update bounds checking feature for subrange streams.

    • Thanks to Aaron Carroll, Amos Robinson, and Vivian Ye-Ting Dang for their bug reports.

  • Fix issue in MUST set generation when a single MIVC is computed.

  • Accept fractions in JSON input for interpreter.

  • Other bug fixes.

Changes:

  • Always check node calls are safe, not only in compositional mode.

  • Set check_subproperties flag to true by default.

    • Ignored if modular analysis is true.

  • Abstract call only if contract has at least one guarantee or one mode.

Kind 2 v1.3.1

This release includes performance improvements and various fixes. Notably:

  • Fix soundness issue in path compression when there are temporal dependencies between input values.

    • Thank you to M. Anthony Aiello for finding this bug.

  • Fix bug in extraction of an active path during IC3 generalization.

  • Improve IC3 performance over large models that contain reals or machine integers.

  • Fix issue reading models from the latest version of Z3 (4.8.10). It caused a runtime error during IVC generation.

Kind 2 v1.3.0

New features:

  • Computation of Inductive Validity Cores and Minimal Cut Sets.

  • Invariant generation for machine integers.

    • Engine names: INVGENMACH and INVGENMACHOS.

  • IC3 model checking engine for machine integers.

    • The pre-image computation is based on quantifier elimination over bit-vectors.

    • It requires SMT solver Z3 at this time.

  • Support for abstract types (#594, thanks to Amos Robinson).

  • Support for SMT solvers Boolector and MathSAT.

    • It requires the develop version of Boolector at this time (commit 5d18baa and later).

  • New command-line option to only parse Lustre inputs (--only_parse true).

Improvements:

  • Support for version 1.8 of SMT solver CVC4.

  • Improved support for machine integers.

  • Reduced number of activation literals used in BMC encoding.

  • Fixed returned exit code for modular analysis (#684).

  • Other bug fixes.

Changes:

  • Removed CZMQ sources and OCaml bindings for CZMQ from the Kind 2 repository.

    • Kind 2 now requires ZMQ 4.x or later to be installed on your system.

  • Replaced old build system with new one based on dune and OPAM.

    • See README file for new requirements and installation instructions.

Kind 2 v1.2.0

New features:

Many bug fixes!

Kind 2 v1.1.0

This new version features many internal improvements as well as several new features over v1.0.1 (more than 300 commits):

  • Support for Scade 6 automata (see documentation)

  • Support for Scade 6 arrays

  • Arithmetic invariant generation: up to v1.0.1, the main invariant generation technique besides the IC3 engine was boolean template-based invariant generation. This technique can discover equalities and implications between predicates over the state variables of the system.

    The technique has been extended to arithmetic terms (int and real): Kind 2 can discover equalities and orderings (<=) between arithmetic terms mined from the input system.

    The boolean, integer and real template-based invariant generation techniques all come in two flavors: one-state which can only relate terms over the current state, and two-state which can relate terms mentioning the current and the previous state.

    Each of them runs as a different process at runtime. By default, only the following are active:

    • INVGENOS (one-state boolean)

    • INVGEN (two-state boolean)

    • INVGENINTOS (one-state integer)

    • INVGENREALOS (one-state real)

  • Several features distinct from the actual verification process were introduced in Kind 2 v1.0.0: certification, contract generation, compilation to Rust, and test generation.

    These features are now aggregated under the term post-analyses. Most of them have been improved and v1.1.0 introduces a post-analysis: invariant logging. This feature attempts to log strengthening invariants discovered by Kind 2 as a contract.

  • Silent contract loading attempts to load contracts generated by Kind 2 during previous runs as candidate properties for the current run (see documentation)

Kind 2 v1.0.1

  • Read files on standard input in Lustre format

Kind 2 v1.0.0

This new version brings many new features and improvements over v0.8 (more than 800 commits).

NB:

  • Kind 2 now requires OCaml 4.03 or higher

New features:

  • 2-induction: makes Kind 2 react quicker to good strengthening invariants discovered by invariant generation

  • Assume/guarantee-based contract language with modes as Lustre annotations (see documentation)

    • specification-checking: before checking a node with a contract, check that the modes from the contract cover all situations allowed by the assumptions (implementation-agnostic mode exhaustiveness)

  • Compositional reasoning: --compositional (see contract semantics)

    • abstraction of subnodes by their contract

  • Modular analyses: --modular

    • Kind 2 traverses the node hierarchy bottom-up

    • applying the analysis specified by the other flags to each node

    • reusing results (invariants) from previous analyses when relevant

    • allows refinement when used with compositional reasoning

  • Compilation from Lustre to Rust: --compile

  • Mode-based test generation: --testgen

    • explores the DAG of activeable modes from the initial state up to a depth

    • generates witnesses as traces of inputs logged as XML files

    • compiles the contract as an executable oracle in Rust: reads a sequence of inputs/outputs values for the original node on stdin and prints on stdout the boolean values the different parts of the contract evaluate to

  • Generation of certificates and proofs: --proof and --certif

    • produces either SMTLIB-2 certificates or LFSC proofs

    • distributed with LFSC proof rules for k-induction

    • requires CVC4, JKind and the LFSC checker for proofs

    • generate proofs skeletons for potential holes

  • Support for forward references on nodes, types, constants and contracts

  • Output and parser for native (internal) transition system format

  • Contract generation: --contract_gen

    • Very experimental: the modes generated might not be exhaustive and the check exhaustiveness check might fail

    • This feature's main goal, for now, is to help users get started with contracts by generating a contract stub partially filled with invariants discovered by invariant generation

Improvements:

  • Flags are now organized into modules, see --help and --help_of <module>

  • Mode information (when available) to counterexample output

  • Optimized invariant generation

  • Named properties and guarantees

  • Colored output

  • No more dependencies on Camlp4

  • Strict mode to disallow unguarded pre and undefined local variables

  • Many bug fixes and performance improvements

  • Added mode information (when available) to counterexample output

  • Rewrote invariant generation from scratch: much faster now

  • czmq fixes: there should be no process still running after Kind 2 exits

Refer to the user documentation online for more details.

Kind 2 v0.8.0

  • Optimize IC3/PDR engine, add experimental IC3 with implicit abstraction

  • Add two modular versions of the graph-based invariant generation from PKind.

  • Add path compression in k-induction

  • Support Yices 1 and 2 as SMT solvers

  • Optimize Lustre translation and internal term data structures

  • Optimize queries to SMT solvers with check-sat with assumption instead of push/pop

  • Return Lustre counterexamples faithful to input by undoing optimizations in translation

  • Improve output and logging

  • Many bug and performance fixes

  • Web service to accept jobs from remote clients

Refer to the user documentation for more details.

OCaml

Innovation. Community. Security.