Kind 2 v1.5.0
In addition to several improvements and bug fixes, this release includes the following new functionalities:
- 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
).
Thanks to M. Anthony Aiello, Andreas Katis, and Amos Robinson for their feedback and suggestions.
Please refer to the CHANGES file for a more detailed description and to the user documentation for more details.
N.B. To run the Ubuntu and macOS binaries the ZeroMQ library (version 4.x or later) must be installed on your computer. You can install it by running sudo apt-get install libzmq5
in Ubuntu, or brew install zmq
in macOS.