K is an executable modular framework for programming language semantics, design and analysis. Learn more about K at its official K Framework site. This Googlecode website hosts a prototype tool that supports most of the K features. There are two ways to obtain it:

• Download and set up a pre-configured virtual machine, following the instructions under the Downloads tab above; or
• Download and install its source code (it uses several languages), following the Source tab above and the instructions in the INSTALL file.

Unless you are a K tool developer, or intend to extend the K tool, we recommend that you use the virtual machine approach.

Mailing List

Subscribe to the K user list for news on major tool updates and questions. For bugs and feature requests, please use the Issues interface.

Related Projects

• C Semantics. A semantics of C using K.
• Matching logic. This project builds a program verification framework on top of K.