Executing Formal Semantics with the K Tool

Lazar, DavidArusoaie, AndreiSerbanuta, Traian FlorinEllison, ChuckyMereuta, RaduLucanu, DorelRoşu, Grigore
FM’12

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