A constructor-based reachability logic for rewrite theories

DOI10.1007/978-3-319-94460-9_12MaRDI QIDQ1671153zbMATH OpenOpenAlexFDO

Authors Stephen Skeirik, José Meseguer, A. Stefanescu

Publication date 6 September 2018

Full work available at URL https://arxiv.org/abs/1709.05045

zbMATH Keywords

program verificationreachability logicrewriting logic

Mathematics Subject Classification ID

Temporal logic (03B44) Logic in computer science (03B70) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Grammars and rewriting systems (68Q42) Specification and verification (program logics, model checking, etc.) (68Q60)

Abstract: Reachability logic has been applied to $mathbbK$ rewrite-rule-based language definitions as a language-generic logic of programs. To be able to verify not just code but also distributed system designs, a new rewrite-theory-generic reachability logic is presented and proved sound for a wide class of rewrite theories. The logic's automation is increased by means of constructor-based semantic unification, matching, and satisfiability procedures. New methods for proving invariants of possibly never terminating distributed systems are developed, and experiments with a prototype implementation illustrating the new proof methods are presented.

Recommendations

• A constructor-based reachability logic for rewrite theories
• Verifying Reachability-Logic Properties on Rewriting-Logic Specifications
• One-path reachability logic

Cited in

(9)

• A coinductive approach to proving reachability properties in logically constrained term rewriting systems
• (Co)inductive proof systems for compositional proofs in reachability logic
• Capturing constrained constructor patterns in matching logic
• Generalized rewrite theories, coherence completion, and symbolic methods
• Programming and symbolic computation in Maude
• Verifying Reachability-Logic Properties on Rewriting-Logic Specifications
• A constructor-based reachability logic for rewrite theories
• Connecting Constrained Constructor Patterns and Matching Logic
• Verification of the IBOS Browser Security Properties in Reachability Logic

This page was built for publication: A constructor-based reachability logic for rewrite theories

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1671153)