Matching Logic
From FSL
Operational semantics are typically used to derive concrete program behaviors, but not to specify and prove properties about programs. The latter are traditionally done using axiomatic semantics. Unfortunately, axiomatic semantics of real languages are rather complex, so correctness proofs are necessary in order to trust the proven properties. Moreover, such proofs have to be maintained as the language changes, which is generally perceived as a burden. Ideally, we would like to have one language semantics, with that semantics used both for deriving program behaviors and for verifying programs.
Matching logic allows us to regard a language through both operational and axiomatic lenses at the same time, making no distinction between the two. A programming language is given a semantics as a set of rewrite rules. A language-independent proof system can then be used to derive both operational behaviors and formal properties of a program. In other words, one matching logic semantics fulfills the roles of both operational and axiomatic semantics in a uniform manner. The state structure plays a crucial role in matching logic semantics. Program states are represented as algebraic datatypes called (concrete) configurations, while program state specifications are represented as configuration terms, with variables and constraints over them, called (configuration) patterns. A pattern specifies those configurations that match it.
Quick Overview
- HERE is the K and matching logic webpage at UIUC, which contains slides and an inteview.
- Older slides: status in June 2011
PPTX 
PDF ; status at the end of 2010: PPTX PDF .
Download and Online Interface
We have implemented a proof-of-concept matching logic verifier for a fragment of C, called MatchC.
-
--- This link provides an online interface to running MatchC
- Download --- We recommend to first try it online (see the link above)
- Old implementations --- Normally you should not need these
-
Select Publications
Click on Publications in the left menu for all our publications related to matching logic. Here are the most relvant:
- The theoretical foundations of matching logic and the implementation of MatchC:
- A short paper on a previous version of MatchC, which used Hoare-style annotations:
- Matching Logic: A New Program Verification Approach (NIER Track)
- Grigore Rosu and Andrei Stefanescu
ICSE'11, ACM, pp. 868-871. 2011
PDF, Slides(pptx), Slides(pdf), Poster(pptx), Poster(pdf), Matching Logic, ACM, NIER ICSE'11, BIB
- Using matchig logic as a program logic in the context of axiomatic semantics:
- Matching Logic: An Alternative to Hoare/Floyd Logic
- Grigore Rosu, Chucky Ellison and Wolfram Schulte
AMAST'10, LNCS 6486, pp 142-162. 2010
PDF, Slides(PPT), Slides(PDF), LNCS, AMAST'10, BIB
Publications
Below are all our publications on matching logic, in reverse chronological order.
- Towards a Unified Theory of Operational and Axiomatic Semantics
- Grigore Rosu and Andrei Stefanescu
ICALP'12, LNCS, to appear. 2012
PDF, Matching Logic, ICALP'12, BIB- Checking Reachability using Matching Logic
- Grigore Rosu and Andrei Stefanescu
PDF, Matching Logic, TR@UIUC, BIB- From Hoare Logic to Matching Logic
- Grigore Rosu and Andrei Stefanescu
PDF, Matching Logic, TR@UIUC, BIB- The Rewriting Logic Semantics Project: A Progress Report
- Jose Meseguer and Grigore Rosu
FCT'11, LNCS 6914, pp 1-37. Invited talk. 2011
PDF, K Tool, FCT'11, BIB- Matching Logic: A New Program Verification Approach (NIER Track)
- Grigore Rosu and Andrei Stefanescu
ICSE'11, ACM, pp. 868-871. 2011
PDF, Slides(pptx), Slides(pdf), Poster(pptx), Poster(pdf), Matching Logic, ACM, NIER ICSE'11, BIB- Matching Logic: A New Program Verification Approach
- Grigore Rosu and Andrei Stefanescu
UV'10. 2010
PDF, Slides(pptx), Slides(pdf), Matching Logic, K framework, UV'10, BIB- Matching Logic: An Alternative to Hoare/Floyd Logic
- Grigore Rosu, Chucky Ellison and Wolfram Schulte
AMAST'10, LNCS 6486, pp 142-162. 2010
PDF, Slides(PPT), Slides(PDF), LNCS, AMAST'10, BIB- From Rewriting Logic Executable Semantics to Matching Logic Program Verification
- Grigore Rosu, Chucky Ellison and Wolfram Schulte
Technical Report http://hdl.handle.net/2142/13159, July 2009
PDF, TR@UIUC, BIB- Matching Logic --- Extended Report
- Grigore Rosu and Wolfram Schulte
Technical Report UIUCDCS-R-2009-3026, January 2009
TR@UIUC, BIB
