Verifying Reachability-Logic Properties on Rewriting-Logic Specifications
DOI10.1007/978-3-319-23165-5_21zbMATH Open1321.68359OpenAlexW2293504102MaRDI QIDQ2945720FDOQ2945720
Vlad Rusu, Andrei Arusoaie, Dorel Lucanu, David 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
Recommendations
- Publication:2722043
- A Verification Logic for Rewriting Logic
- Rewriting logic as a framework for generic verification tools
- A constructor-based reachability logic for rewrite theories
- A constructor-based reachability logic for rewrite theories
- Rewriting Techniques and Applications
- scientific article; zbMATH DE number 1231544
- Verification from Declarative Specifications Using Logic Programming
Grammars and rewriting systems (68Q42) Specification and verification (program logics, model checking, etc.) (68Q60) Logic in computer science (03B70) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)
Cites Work
- All about Maude -- a high-performance logical framework. How to specify, program and verify systems in rewriting logic. With CD-ROM.
- K-Java: a complete semantics of Java
- An overview of the K semantic framework
- Algebraic simulations
- Conditional rewriting logic as a unified model of concurrency
- Twenty years of rewriting logic
- Semantic foundations for generalized rewrite theories
- The Maude LTL model checker
- Rewriting Modulo SMT and Open System Analysis
- Abstract Logical Model Checking of Infinite-State Systems Using Narrowing
- Towards a Unified Theory of Operational and Axiomatic Semantics
- From Hoare Logic to Matching Logic Reachability
- The rewriting logic semantics project
- Equational abstractions
- All-Path Reachability Logic
- One-Path Reachability Logic
- Language Definitions as Rewrite Theories
- Proving Safety Properties of Rewrite Theories
Cited In (15)
- Generalized rewrite theories, coherence completion, and symbolic methods
- A Verification Logic for Rewriting Logic
- (Co)inductive proof systems for compositional proofs in reachability logic
- Metalevel algorithms for variant satisfiability
- Specification inference using context-free language reachability
- Rewriting logic as a framework for generic verification tools
- Programming and symbolic computation in Maude
- Abstract Certification of Global Non-interference in Rewriting Logic
- Specifying program properties using modal fixpoint logics: a survey of results
- A generic framework for symbolic execution: a coinductive approach
- QMaude: quantitative specification and verification in rewriting logic
- Title not available (Why is that?)
- Unification in matching logic
- Proving Reachability-Logic Formulas Incrementally
- Verification of the IBOS Browser Security Properties in Reachability Logic
Uses Software
This page was built for publication: Verifying Reachability-Logic Properties on Rewriting-Logic Specifications
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2945720)
