Projects
From K Framework
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
[edit] 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.
