×

K-Maude

swMATH ID: 9747
Software Authors: Şerbănuţă, Traian Florin; Roşu, Grigore
Description: 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.
Homepage: http://link.springer.com/chapter/10.1007%2F978-3-642-16310-4_8
Related Software: Maude; K Prover; K tool; OBJ3; K-Java; Elf; DDebugger; CafeOBJ; KOOL; JavaFAN; LambdaMu-calculus; Archive Formal Proofs; GitHub; KJS; Toolchain; LLVM; Isabelle; Coq; CITP; CafeInMaude
Referenced in: 10 Publications

Referencing Publications by Year