K project was started in 2003 by Grigore Rosu, University of Illinois at Urbana Champaign (UIUC), for teaching puposes. Starting with 2010, K became a joint work between Formal Systems Laboratory (FSL) from UIUC and Formal Methods in Software Engineering (FMSE) groupfrom Al. I. University of Iasi (UAIC).
In the new perspective, K is envisioned as an executable semantic framework in which programming languages together with their type systems or formal analysis tools can be defined. The goal is that K Framework to be equally used by academia and industry. The main components of a K definition consist of configurations, computations and rules. Configurations abstractly describe the machine which on the programs/systems are exectued; the system/program state is organized into hierarchical structure of units, called cells. Computations are structures carrying computational meaning by sequentializing the computational tasks, such as fragments of program. K (rewrite) rules generalize conventional rewrite rules by making explicit which parts of the term they read, write, or do not care about.
In this talk we give a light introduction to K using two toy examples. The first one is a kernel of C, called Cink, for which we give an executable formal definition, incrementally developed, and a static analyser derived from the definition and whic is able to find infinite loops and infeasible paths in the control flow graph. The second example is a simple language modeling the object creation, inspired from the paper "Symbolic Execution of Unbounded Object Creation" by Jurriaan Rot, Frank de Boer, and Marcello Bonsangue. We show that how the abstratct semantics and the symbolic one are derived from the definition of the model. The executabilty of all examples will be demonstrated with the K Maude prototype.
A fully description of K can be found in: Traian Florin Serbanuta. A Rewriting Approach to Concurrent Programming Language Design and Semantics. PhD Thesis, University of Illinois, December 2010 (http://fsl.cs.uiuc.edu/pubs/serbanuta-2010-thesis.pdf) and Grigore Rosu and Traian Florin Serbanuta. An Overview of the K Semantic Framework. J.LAP, Volume 79(6), pp 397-434. 2010 (http://fsl.cs.uiuc.edu/pubs/rosu-serbanuta-2010-jlap.pdf)
The K Maude prototype project is hosted on Google Code: http://code.google.com/p/k-framework/ and described in Traian Florin Serbanuta and Grigore Rosu. K-Maude: A Rewriting Based Tool for Semantics of Programming Languages WRLA'10, LNCS 6381, pp 104-122. 2010 (http://fsl.cs.uiuc.edu/pubs/serbanuta-rosu-2010-wrla.pdf)