A Rewriting-Based Model Checker for the Linear Temporal Logic of Rewriting
From MaRDI portal
Publication:5166636
DOI10.1016/j.entcs.2012.11.009zbMath1291.68244WikidataQ113318033 ScholiaQ113318033MaRDI QIDQ5166636
Publication date: 27 June 2014
Published in: Electronic Notes in Theoretical Computer Science (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/j.entcs.2012.11.009
68Q60: Specification and verification (program logics, model checking, etc.)
68Q42: Grammars and rewriting systems
03B44: Temporal logic
Related Items
Unnamed Item, Compositional Specification in Rewriting Logic, Model Checking TLR* Guarantee Formulas on Infinite Systems, A Spatial Logic for Simplicial Models, Enabling synchronous and asynchronous communications in CSP for SOC, Comparing three coordination models: Reo, ARC, and PBRD, Twenty years of rewriting logic, Egalitarian State-Transition Systems, Model Checking Reconfigurable Petri Nets with Maude
Uses Software
Cites Work
- A state/event-based model-checking approach for the analysis of abstract system properties
- Results on the propositional \(\mu\)-calculus
- The rewriting logic semantics project
- Maude's module algebra
- All about Maude -- a high-performance logical framework. How to specify, program and verify systems in rewriting logic. With CD-ROM.
- Conditional rewriting logic as a unified model of concurrency
- Maude: specification and programming in rewriting logic
- Equational rules for rewriting logic
- A spatial logic for concurrency. II
- A spatial logic for concurrency. I
- Concurrent software verification with states, events, and deadlocks
- Semantic foundations for generalized rewrite theories
- A Verification Logic for Rewriting Logic
- The Temporal Logic of Rewriting: A Gentle Introduction
- Algebraic laws for nondeterminism and concurrency
- Foundations of Software Science and Computation Structures
- Symbolic Model Checking of Logics with Actions
- State/Event Software Verification for Branching-Time Specifications
- Automated Deduction – CADE-19
- Integrated Formal Methods
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item