# Difference between revisions of "Matching Logic: An Alternative to Hoare Logic"

From FSL

Line 1: | Line 1: | ||

− | <purge></purge> | + | <purge></purge><private>== AMAST'10 ==</private><pub id="rosu-ellison-schulte-2010-amast" template="PubDefaultWithAbstractAndTitle"> </pub> |

− | <private>== AMAST'10 ==</private><pub id="rosu-ellison-schulte-2010-amast" template="PubDefaultWithAbstractAndTitle"> </pub> | + | <private>==Submitted to AMAST'10==</private><pub id='rosu-ellison-schulte-2010-amast-submission' template='PubDefaultWithAbstractAndTitle'></pub> |

− | <private>==Submitted to AMAST'10==</private> | + | <private>==Submitted to LICS'10==</private><pub id='rosu-ellison-schulte-2010-lics-submission' template='PubDefaultWithAbstractAndTitle'></pub> |

− | <pub id='rosu-ellison-schulte-2010-amast-submission' template='PubDefaultWithAbstractAndTitle'></pub> | + | <private>==Submitted to ESOP'10==</private><pub id='rosu-ellison-schulte-2010-esop' template='PubDefaultWithAbstractAndTitle'></pub> |

− | <private>==Submitted to LICS'10==</private> | + | |

− | <pub id='rosu-ellison-schulte-2010-lics-submission' template='PubDefaultWithAbstractAndTitle'></pub> | + | |

− | <private>==Submitted to ESOP'10==</private> | + | |

− | <pub id='rosu-ellison-schulte-2010-esop' template='PubDefaultWithAbstractAndTitle'></pub> | + |

## Revision as of 17:23, 23 December 2010

**Matching Logic: An Alternative to Hoare/Floyd Logic**- Grigore Rosu, Chucky Ellison and Wolfram Schulte
, LNCS 6486, pp 142-162. 2010**AMAST'10**

*Abstract.*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.

- PDF, Slides(PPT), Slides(PDF), LNCS, AMAST'10, BIB