Matching logic: An alternative to Hoare/Floyd logic

Grigore Roşu, Chucky Ellison, Wolfram Schulte

Research output: Chapter in Book/Report/Conference proceedingConference contribution


This paper introduces matching logic, a novel framework for defining axiomatic semantics for programming languages, inspired from operational semantics. Matching logic specifications are particular first-order formulae with constrained algebraic structure, called patterns. Program configurations satisfy patterns iff they match their algebraic structure and satisfy their constraints. Using a simple imperative language (IMP), it is shown that a restricted use of the matching logic proof system is equivalent to IMP's Hoare logic proof system, in that any proof derived using either can be turned into a proof using the other. Extensions to IMP including a heap with dynamic memory allocation and pointer arithmetic are given, requiring no extension of the underlying first-order logic; moreover, heap patterns such as lists, trees, queues, graphs, etc., are given algebraically using fist-order constraints over patterns.

Original languageEnglish (US)
Title of host publicationAlgebraic Methodology and Software Technology - 13th International Conference, AMAST 2010, Revised Selected Papers
Number of pages21
StatePublished - 2011
Event13th International Conference on Algebraic Methodology and Software Technology, AMAST 2010 - Lac-Beauport, QC, Canada
Duration: Jun 23 2010Jun 25 2010

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume6486 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Other13th International Conference on Algebraic Methodology and Software Technology, AMAST 2010
CityLac-Beauport, QC

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)


Dive into the research topics of 'Matching logic: An alternative to Hoare/Floyd logic'. Together they form a unique fingerprint.

Cite this