Language definitions as rewrite theories

DOI10.1016/j.jlamp.2015.09.001zbMath1356.68125OpenAlexW2079991001MaRDI QIDQ730476

Traian-Florin Şerbănuţă, Dorel Lucanu, Vlad Rusu, Grigore Roşu, Andrei Ştefănescu, Andrei Arusoaie

Publication date: 28 December 2016

Published in: Journal of Logical and Algebraic Methods in Programming (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.jlamp.2015.09.001

zbMATH Keywords

operational semanticssymbolic executionMaudeK frameworkrewrite theories

Mathematics Subject Classification ID

Semantics in the theory of computing (68Q55) Grammars and rewriting systems (68Q42) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items

Executing and verifying higher-order functional-imperative programs in Maude, A generic framework for symbolic execution: a coinductive approach, A Maude environment for CafeOBJ, A partial evaluation framework for order-sorted equational programs modulo axioms

Uses Software

• z3
• Maude
• K tool
• K-Maude
• K Prover

Cites Work

• Equational abstractions
• An overview of the K semantic framework
• All about Maude -- a high-performance logical framework. How to specify, program and verify systems in rewriting logic. With CD-ROM.
• Equational rules for rewriting logic
• On the Church-Rosser and coherence properties of conditional order-sorted rewrite theories
• Language Definitions as Rewrite Theories
• Rewriting Modulo SMT and Open System Analysis
• State Space Reduction of Rewrite Theories Using Invisible Transitions
• K-Maude: A Rewriting Based Tool for Semantics of Programming Languages
• One-Path Reachability Logic
• Matching Logic - Extended Abstract (Invited Talk)