K-user mailing list

[Dwight Guth <dwight.guth AT gmail.com>]

K version 3.5 has been released! This release, continuing from the 3.4 release in August, adds a number of new features, especially concerning program verification, speed enhancements, the ability for third party developers to create plug-in features for the framework, and more. Several old features are also discontinued. For the complete list of changes, refer to CHANGELOG.md in the root of the distribution. You can download the release from Github.

This release will be the first release of the framework to feature long-term support. Developers at Runtime Verification, Inc. will be responding to bug reports submitted on Github in order to fix bugs and backport some new features on a case-by-case basis. While we do not guarantee that we will always agree to your support request, priority will be given to requests which can demonstrate an inability to upgrade their K definition to the 3.6.x development version.

NOTE: K 3.5 is the last version of the K framework to support the Maude backend. In the past several months, the stability and usability of the new Java rewrite engine has been greatly improved. In particular, the performance improvements have been quite dramatic, increasing the speed of running all 700 C examples in the C semantics GCC torture test from several hours to under 15 minutes. We encourage all users to attempt to port their definitions and file issues on Github where they run into trouble, and users who report issues with K 3.5 will be first encouraged to try to upgrade their definition and only if that fails, to document the bug to be fixed. We hope to continue to improve the Java rewriter until it is able to support every definition that was supported by the old Maude backend. Once this is complete, we will release K 4.0 and discontinue support of K 3.5.

Thanks for continuing to use K, and we hope you will be satisfied with the improvements we've made to it!

Dwight Guth

Principal K Engineer

Runtime Verification, Inc.