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

first-order logicprogram logicrewritingverification

Mathematics Subject Classification ID

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

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

(17)

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

Describes a project that uses

Uses Software

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

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)