A constructor-based reachability logic for rewrite theories

DOI10.1007/978-3-319-94460-9_12zbMath1471.68075arXiv1709.05045OpenAlexW3027204833MaRDI QIDQ1671153

Stephen Skeirik, José Meseguer, Andrei Ştefănescu

Publication date: 6 September 2018

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

zbMATH Keywords

program verificationrewriting logicreachability logic

Mathematics Subject Classification ID

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

Related Items (5)

(Co)inductive proof systems for compositional proofs in reachability logic ⋮ All-Path Reachability Logic ⋮ Generalized rewrite theories, coherence completion, and symbolic methods ⋮ Programming and symbolic computation in Maude ⋮ Capturing constrained constructor patterns in matching logic

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