k-framework

The K Semantic Framework

We moved!
Check us out on https://github.com/kframework'>Github!

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.

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