Executing Formal Semantics with the double-struck K Tool

David Lazar, Andrei Arusoaie, Traian Florin Şerbǎnuţǎ, Chucky Ellison, Radu Mereuta, Dorel Lucanu, Grigore Roşu

Research output: Chapter in Book/Report/Conference proceedingConference contribution


This paper describes the double-struck K Tool, a system for formally defining programming languages. Formal definitions created using the double-struck K Tool automatically yield an interpreter for the language, as well as program analysis tools such as a state-space explorer. The modularity of double-struck K and the design of the tool allow one semantics to be used for several applications.

Original languageEnglish (US)
Title of host publicationFM 2012
Subtitle of host publicationFormal Methods - 18th International Symposium, Proceedings
Number of pages5
StatePublished - 2012
Event18th International Symposium on Formal Methods, FM 2012 - Paris, France
Duration: Aug 27 2012Aug 31 2012

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume7436 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Other18th International Symposium on Formal Methods, FM 2012

ASJC Scopus subject areas

  • Theoretical Computer Science
  • General Computer Science


Dive into the research topics of 'Executing Formal Semantics with the double-struck K Tool'. Together they form a unique fingerprint.

Cite this