Formal Methods in Software Engineering

The K Primer (version 3.2)

Year2013
TypeConference
StatusProceedings
AuthorsTraian Serbanuta, Andrei Arusoaie, Unknown, Chucky Ellison, Dorel Lucanu, Grigore Rosu

Links

Abstract

This paper serves as a brief introduction to the K tool, a system for formally defining programming languages. It is shown how sequential or concurrent languages can be defined in K simply and modularly. These formal definitions automatically yield an interpreter for the language, as well as program analysis tools such as a state-space explorer.

BibTeX

@inproceedings{k-primer-2012-v25, author = {Traian Florin Serbanuta and Andrei Arusoaie and David Lazar and Chucky Ellison and Dorel Lucanu and Grigore Rosu}, title = {The K Primer (version 3.2)}, editor = {Mark Hills}, booktitle = {K'11}, series = {ENTCS}, year = {2013}, note = {to appear}, url = {http://www.kframework.org/K11/[K11]}, }