Kind 2 v2.3.0
New features:
- Support for polymorphic user types, nodes, functions, and contracts
- New
transparent and opaque modifiers to control the abstraction and refinement of nodes and functions - Support for function calls with arguments that contain quantified variables and symbolic indices, if they can be inlined
- Support for OpenSMT as a backend solver
Improvements:
- Support for system parameters with refinement types
- Option (
--lus_main_type) to specify a refinement type for realizability analysis - Ensure results are printed in JSON/XML output, even if computation of deadlocking trace fails
- Fixed bugs when checking the realizability of a node's environment
- Fixed bug when the
history type constructor was used in a contract - Fixed and improved the handling of array definitions and quantified expressions
- Fixed several bugs related to casting machine integers to integers
- Other fixes and improvements in the Lustre front end
Changes:
- Allow calls to nodes and functions with both a body and a contract
Kind 2 v2.2.0
New features:
Improvements:
- Optimized encoding of counters in reachability queries
- Fixed issue where checks on assumptions of called nodes were not instantiated if an intermediate node has no properties
- The new version applies slicing per IC3IA engine instance
Changes:
- For imported nodes and functions, Kind 2 now assumes conservatively that each output stream depends on the current values of all inputs. The user must refine the model to avoid false positives of circular dependencies
- A call to a node without a contract but with at least one output that has a subrange type is now abstracted. Subrange types are now treated as a special case of refinement types, handled as an extension of the contract's node, or as the sole specification if none is provided
- Undefined initial values and values of undefined output streams with a subrange type range over the base integer type
- The type of constants must be provided in their declaration
- Invariant generation engines now always start generating invariants from the top
Kind 2 v2.1.1
This release includes some minor improvements and various fixes. Notably:
- Fix soundness bug in IC3IA engine
- Allow variables with subrange types in the interface of a contract node
- Accept new versions of cvc5 for proof production (up to 1.1.0)
Kind 2 v2.1.0
This release includes multiple improvements and bug fixes. Notably:
- Add new option for printing the set of viable states of a realizable contract (
--print_viable_states). - Allow the second argument of a shift operator to be non-constant.
- Add support for the latest versions of SMT solver Bitwuzla (v0.1.1 and above).
- Fix compatibility issue with OCaml 5.0.0+
- Fix printing of values of stateless variables in counterexamples (bug introduced in v2.0.0).
- Fix several bugs related to the definition and use of arrays in Lustre models.
- Add static checks on the definition of global subrange constants.
- Accept
param keyword for the declaration of system parameters (global constants without a definition). - Add subrange and enum constraints on system parameters.
- Fix type checking and handling of constant node arguments.
- Other improvements and bug fixes in the Lustre front end.
Kind 2 v2.0.0
New features:
Improvements:
Changes:
- Add
--exit_code_mode option to control exit code convention.
Kind 2 v1.9.0
New features:
Improvements:
- Fix underreporting issue in the computation of conflicting constraints (bug introduced in v1.6.0).
- Fix reporting of contract mode elements in IVCs and conflicting constraints (bug introduced in v1.8.0).
- Fix setting of SMT-LIB logic for the non-linear combination of integers and reals.
- Fix computation of dependencies for clock operators in new the Lustre front end.
- Other fixes and improvements in the new front end.
Changes:
Kind 2 v1.8.0
New features:
Improvements:
Kind 2 v1.7.0
New features:
Improvements:
- Support for unary negation and subtraction of unsigned machine integers.
- Fix invariant pruner: some non-trivial one-state invariants were not included in certificates.
- Fix problem with reported locations in IVC output.
- Fix selection of logic in computation of MCS.
- Fix version detection of SMT solvers.
- Multiple fixes and improvements in the new Lustre front end.
Kind 2 v1.6.0
New features:
A new implementation of Kind 2's language front end with:
- Support for forward references to nodes and modes in contracts.
- Individual namespaces for imported contracts.
- Enhanced type checking of composite data types.
Internally, the new implementation follows a multi-pass approach more strictly. This should facilitate the extensibility and maintenance of the new front end. Although we strongly encourage users to use the new front end, the old front end can still be enabled for now by passing --old_frontend true to Kind 2.
Improvements:
- Fix issue where the inductive step check could incorrectly declare a property k-inductive after a contract has been refined in compositional verification.
- Fix bug in minimization of set of invariants.
- Fix XML and JSON output produced by the certificate generation post-analysis.
- Include various updates and fixes to the realizability and satisfiability checks of contracts. Now there is a flag to (de)activate the computation of a deadlocking trace,
--print_deadlock, and a flag to (de)activate the satisfiability check of an unrealizable contract, --check_contract_is_sat.
Changes:
- New default behavior: if no node is marked as a main node, Kind 2 considers all the top nodes for analysis.
- Functional congruence is only enforced on abstract functions when the flag
--enforce_func_congruence is true (default: false). - Make Kind 2 compatible with recent versions of Menhir (20211230 and later).
- Remove two experimental post-analyses: invariant logging and silent contract loading.
- Remove support for automata.
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:
Improvements:
Changes:
Kind 2 v1.3.1
This release includes performance improvements and various fixes. Notably:
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:
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.