From hidden to visible: a unified framework for transforming behavioral theories into rewrite theories

DOI10.1016/j.tcs.2018.01.006zbMath1388.68189OpenAlexW2794415049MaRDI QIDQ1704601

Kazuhiro Ogata, Min Zhang

Publication date: 12 March 2018

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.tcs.2018.01.006

zbMATH Keywords

transformationbehavioral theorylinear-time propertyrewrite theory

Mathematics Subject Classification ID

Abstract data types; algebraic specification (68Q65) Grammars and rewriting systems (68Q42)

Uses Software

• CASL
• SPIN
• PVS
• NuSMV
• Maude
• ITP
• ASF+SDF
• CITP

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Complexity of matching problems
• A hidden agenda
• Logical foundations of CafeOBJ
• CASL: the Common Algebraic Specification Language.
• Partial-order methods for the verification of concurrent systems. An approach to the state-explosion problem
• Principles of proof scores in CafeOBJ
• Twenty years of rewriting logic
• Constructor-Based Inductive Theorem Prover
• Partial Order Reduction for Rewriting Semantics of Programming Languages
• Removing redundant arguments automatically
• Hidden coinduction: behavioural correctness proofs for objects
• Term Rewriting and All That
• Generate & Check Method for Verifying Transition Systems in CafeOBJ
• Computer Aided Verification
• Recent Trends in Algebraic Development Techniques
• Some Tips on Writing Proof Scores in the OTS/CafeOBJ Method
• Formal Methods for Open Object-Based Distributed Systems

This page was built for publication: From hidden to visible: a unified framework for transforming behavioral theories into rewrite theories