Semantics of C in K
Formal Semantics of P4 in K
The K tools
Modeling EVM in the K framework
Formal semantics of LLVM IR in K
The semantics of Java in K
Plugin files for editing K files
A Prototype Formal Semantics of WebAssembly in K
Formal semantics of LLVM IR in K (old)
Cink is a kernel of the C++ language we used to experiment with K. The language is used an example for teaching classes and is referred in several research papers.
Online extensible IDE for the K Framework and other formal verification projects. Example deployment at http://kframework.org/kweb/
GNU MPFR Java Bindings
Semantics of the Java Virtual Machine.
K semantics for the javacard language
An executable algorithmic language. The algorithms are executed over abstract data types like arrays, structures, cons lists (viewed as abstractions of simple linked lists).
Formal semantics of OCaml
Formal semantics of AADL in K
The semantics of Python in K