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:

• Support for machine integers.
• Option to output results in JSON format.
• Interpreter accepts input values in JSON format.

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.