Matching logic

DOI10.23638/LMCS-13(4:28)2017MaRDI QIDQ4600770zbMATH OpenOpenAlexFDO

Authors Grigore Roşu

Publication date 12 January 2018

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

zbMATH Keywords

verificationfirst-order logicrewritingprogram logic

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42) Specification and verification (program logics, model checking, etc.) (68Q60) Logic in computer science (03B70)

Abstract: This paper presents matching logic, a first-order logic (FOL) variant for specifying and reasoning about structure by means of patterns and pattern matching. Its sentences, the patterns, are constructed using variables, symbols, connectives and quantifiers, but no difference is made between function and predicate symbols. In models, a pattern evaluates into a power-set domain (the set of values that match it), in contrast to FOL where functions and predicates map into a regular domain. Matching logic uniformly generalizes several logical frameworks important for program analysis, such as: propositional logic, algebraic specification, FOL with equality, modal logic, and separation logic. Patterns can specify separation requirements at any level in any program configuration, not only in the heaps or stores, without any special logical constructs for that: the very nature of pattern matching is that if two structures are matched as part of a pattern, then they can only be spatially separated. Like FOL, matching logic can also be translated into pure predicate logic with equality, at the same time admitting its own sound and complete proof system. A practical aspect of matching logic is that FOL reasoning with equality remains sound, so off-the-shelf provers and SMT solvers can be used for matching logic reasoning. Matching logic is particularly well-suited for reasoning about programs in programming languages that have an operational semantics, but it is not limited to this.

Recommendations

• Matching logic -- extended abstract (invited talk)
• Matching logic explained
• Matching logic: an alternative to Hoare/Floyd logic
• Connecting Constrained Constructor Patterns and Matching Logic
• From hoare logic to matching logic reachability

Cited in

(14)

• Towards a trustworthy semantics-based language framework via proof generation
• SpeX: a rewriting-based formal specification environment
• Matching logic -- extended abstract (invited talk)
• Matching logic: an alternative to Hoare/Floyd logic
• Interactive matching logic proofs in Coq
• Matching logic explained
• Many-sorted hybrid modal languages
• Difference of constrained patterns in logically constrained term rewrite systems
• Connecting Constrained Constructor Patterns and Matching Logic
• A matching logic foundation for Alk
• Unification in matching logic
• A Non-Deterministic Multiset Query Language
• Matching µ-logic: Foundation of K framework
• Capturing constrained constructor patterns in matching logic

Describes a project that uses

Uses Software

• K Prover
• Python
• jStar
• Smallfoot
• SLAyer
• VCC
• Maude
• CafeOBJ
• z3
• Why3
• CASL
• Isabelle/HOL
• Coq

This page was built for publication: Matching logic

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