From K Framework
Jump to: navigation, search

Here is a list of projects involving K. Send us a message if you want your project listed here. Feel free to contact us or the authors if you are interested in any particular project below.

Traian Florin Serbanuta, Andrei Arusoae, Chucky Ellison, David Lazar, Dorel Lucanu, Radu Mereuta, Grigore Rosu
Collection of K utilities (interpreters, visualizers, state-space searchers, model checkers)
Grigore Rosu, Andrei Stefanescu
Deductive program verification framework based on operational semantics, including K semantics
Andrei Stefanescu, Grigore Rosu
Matching logic program verifier for (a fragment of) C implemented using. It also has an Online Interface
Chucky Ellison
Defining a semantics of C in K
Dorel Lucanu, Vlad Rusu
Formal model-based language engineering using K
Patrick Meredith, Mark Hills
Defining a semantics of Scheme in K
David Lazar
Defining a semantics of Haskell in K
Patrick Meredith, Michael Katelman
Defining a semantics of Verilog in K
David Lazar, Chucky Ellison
Defining a semantics of LLVM IR in K
Chucky Ellison, David Lazar
Formal semantics of esoteric programming languages in K
  • OCAML Compiler for K
Chucky Ellison, Michael Ilseman
Dwight Guth
Formal semantics of Python 3.2 in K
Daniele Filaretti, Sergio Maffeis
Formal semantics of PHP in K

Older Projects

These projects use the K technique or some older version of the K tool.

Mark Hills
Defining a semantics of Beta in K
Feng Chen, Azadeh Farzan
Defining a K semantics of Java 1.4 and the JVM as part of the JavaFAN project
Mark Hills
Defining an experimental OO language designed. It also has an Special:KOOLOnline Online Interface.
Mark Hills
Abstract interpretations for verifying domains specific properties.
Traian Florin Serbanuta, Grigore Rosu
The previous version of the K tool. Normally you should not need this.
Personal tools