K-Maude: A rewriting based tool for semantics of programming languages. K is a rewriting-based framework for defining programming languages. K-Maude is a tool implementing K on top of Maude. K-Maude provides an interface accepting K modules along with regular Maude modules and a collection of tools for transforming K language definitions into Maude rewrite theories for execution or analysis, or into LaTeX for documentation purposes. The current K-Maude prototype was successfully used in defining several languages and language analysis tools, both for research and for teaching purposes. This paper describes the K-Maude tool, both from a user and from an implementer perspective.
Keywords for this software
References in zbMATH (referenced in 11 articles , 1 standard article )
Showing results 1 to 11 of 11.
- Li, Liyi; Gunter, Elsa L.: A complete semantics of (\mathbbK) and its translation to Isabelle (2021)
- Riesco, Adrián; Ogata, Kazuhiro; Futatsugi, Kokichi: A Maude environment for CafeOBJ (2017)
- Rusu, Vlad; Lucanu, Dorel; Şerbănuţă, Traian-Florin; Arusoaie, Andrei; Ştefănescu, Andrei; Roşu, Grigore: Language definitions as rewrite theories (2016)
- Caltais, Georgiana: Expression-based aliasing for OO-languages (2015)
- Asăvoae, Mihail; Asăvoae, Irina Măriuca; Lucanu, Dorel: On abstractions for timing analysis in the (\mathbbK) framework (2012)
- Lazar, David; Arusoaie, Andrei; Şerbǎnuţǎ, Traian Florin; Ellison, Chucky; Mereuta, Radu; Lucanu, Dorel; Roşu, Grigore: Executing formal semantics with the (\mathbbK) tool (2012) ioport
- Meseguer, José: Twenty years of rewriting logic (2012)
- Simmons, Robert J.; Pfenning, Frank: Logical approximation for program analysis (2011)
- Asăvoae, Irina Măriuca; Asăvoae, Mihail: Collecting semantics under predicate abstraction in the K framework (2010)
- Roşu, Grigore; Şerbănuţă, Traian Florin: An overview of the K semantic framework (2010)
- Şerbănuţă, Traian Florin; Roşu, Grigore: K-Maude: a rewriting based tool for semantics of programming languages (2010)