Verifying Reachability-Logic Properties on Rewriting-Logic Specifications

DOI10.1007/978-3-319-23165-5_21zbMath1321.68359OpenAlexW2293504102MaRDI QIDQ2945720

Vlad Rusu, Andrei Arusoaie, Dorel Lucanu, David E. Nowak

Publication date: 14 September 2015

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-319-23165-5_21

Mathematics Subject Classification ID

Logic in computer science (03B70) Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85) Grammars and rewriting systems (68Q42)

Related Items (6)

Metalevel algorithms for variant satisfiability ⋮ A generic framework for symbolic execution: a coinductive approach ⋮ (Co)inductive proof systems for compositional proofs in reachability logic ⋮ Generalized rewrite theories, coherence completion, and symbolic methods ⋮ Programming and symbolic computation in Maude ⋮ Proving Reachability-Logic Formulas Incrementally

Uses Software

• Maude
• K tool
• K-Java
• K Prover

Cites Work

• Unnamed Item
• Algebraic simulations
• The rewriting logic semantics project
• 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.
• Conditional rewriting logic as a unified model of concurrency
• Twenty years of rewriting logic
• Semantic foundations for generalized rewrite theories
• K-Java
• Language Definitions as Rewrite Theories
• Rewriting Modulo SMT and Open System Analysis
• Abstract Logical Model Checking of Infinite-State Systems Using Narrowing
• Proving Safety Properties of Rewrite Theories
• Towards a Unified Theory of Operational and Axiomatic Semantics
• From Hoare Logic to Matching Logic Reachability
• All-Path Reachability Logic
• One-Path Reachability Logic

This page was built for publication: Verifying Reachability-Logic Properties on Rewriting-Logic Specifications