Verifying Reachability-Logic Properties on Rewriting-Logic Specifications

DOI10.1007/978-3-319-23165-5_21MaRDI QIDQ2945720zbMATH OpenOpenAlexFDO

Authors Dorel Lucanu, Vlad Rusu, Andrei Arusoaie, 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

Mathematics Subject Classification ID

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)

Recommendations

• scientific article; zbMATH DE number 1617312
• 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

Cites work

• Abstract logical model checking of infinite-state systems using narrowing
• Algebraic simulations
• All about Maude -- a high-performance logical framework. How to specify, program and verify systems in rewriting logic. With CD-ROM.
• An overview of the K semantic framework
• Conditional rewriting logic as a unified model of concurrency
• Equational abstractions
• From hoare logic to matching logic reachability
• K-Java: a complete semantics of Java
• Language definitions as rewrite theories
• One-path reachability logic
• Proving Safety Properties of Rewrite Theories
• Rewriting modulo SMT and open system analysis
• Semantic foundations for generalized rewrite theories
• The Maude LTL model checker
• The rewriting logic semantics project
• Towards a unified theory of operational and axiomatic semantics
• Twenty years of rewriting logic

Cited in

(18)

• Generalized rewrite theories, coherence completion, and symbolic methods
• Simulation and verification of synchronous set relations in rewriting logic
• 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
• A constructor-based reachability logic for rewrite theories
• Programming and symbolic computation in Maude
• Abstract Certification of Global Non-interference in Rewriting Logic
• Proving reachability-logic formulas incrementally
• 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
• scientific article; zbMATH DE number 1617312 (Why is no real title available?)
• A constructor-based reachability logic for rewrite theories
• Unification in matching logic
• Verification of the IBOS Browser Security Properties in Reachability Logic

Describes a project that uses

Uses Software

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

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)