License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.RTA.2015.5
URN: urn:nbn:de:0030-drops-51859
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2015/5185/
Go to the corresponding LIPIcs Volume Portal

Rosu, Grigore

Matching Logic - Extended Abstract (Invited Talk)

pdf-format:
5.pdf (0.6 MB)

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, 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, at the same time admitting its own sound and complete proof system. A practical aspect of matching logic is that FOL reasoning 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 a rewrite-based operational semantics.

BibTeX - Entry

@InProceedings{rosu:LIPIcs:2015:5185,
  author =	{Grigore Rosu},
  title =	{{Matching Logic - Extended Abstract (Invited Talk)}},
  booktitle =	{26th International Conference on Rewriting Techniques and Applications (RTA 2015)},
  pages =	{5--21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-85-9},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{36},
  editor =	{Maribel Fern{\'a}ndez},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2015/5185},
  URN =		{urn:nbn:de:0030-drops-51859},
  doi =		{10.4230/LIPIcs.RTA.2015.5},
  annote =	{Keywords: Program logic, First-order logic, Rewriting, Verification}
}

Keywords: Program logic, First-order logic, Rewriting, Verification
Collection: 26th International Conference on Rewriting Techniques and Applications (RTA 2015)
Issue Date: 2015
Date of publication: 18.06.2015

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI