Matching Logic
Operational semantics are typically used to derive concrete program behaviours, 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 behaviours 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 behaviours and formal properties of a program. In other words, one matching logic semantics fulfils 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
- Latest:
PPTX 
PDF
- The K and Matching Logic webpage at UIUC, which contains slides and an interview.
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)
-
We have formalized the proof system in Coq, including the soundness proof and applications. The Coq latest files are available here.
Select Publications
Here are the most relevant publications on matching logic:
- A language-independent proof system for all-path reachability, with soundness and relative completeness proofs
- All-Path Reachability Logic
- Andrei Stefanescu and Stefan Ciobaca and Radu Mereuta and Brandon Moore and Traian Florin Serbanuta and Grigore Rosu
RTA'14, LNCS 8560, pp 425-440. 2014
PDF, Slides(PPTX), Matching Logic, DOI, RTA'14, BIB
- A language-independent proof system for one-path reachability which supports semantics given with conditional rules (big-step and small-step), with soundness and relative completeness proofs
- One-Path Reachability Logic
- Grigore Rosu and Andrei Stefanescu and Stefan Ciobaca and Brandon Moore
LICS'13, IEEE, pp 358-367. 2013
PDF, Slides(PPTX), Reachability Logic, LICS'13, BIB
- A language-independent program verification framework, including the MatchC verifier:
- Checking Reachability using Matching Logic
- Grigore Rosu and Andrei Stefanescu
OOPSLA'12, ACM, pp 555-574. 2012
PDF, Slides(PPTX), Slides(PDF), Matching Logic, DOI, OOPSLA'12, BIB
- The relationship to Hoare logic, including a mechanical translation of Hoare logic proofs into matching logic proofs:
- From Hoare Logic to Matching Logic Reachability
- Grigore Rosu and Andrei Stefanescu
FM'12, LNCS 7436, pp 387-402. 2012
PDF, Slides(PPTX), Slides(PDF), Matching Logic, DOI, FM'12, BIB
Other
Older slides
Old implementations
Complete list of Publications (reverse chronological order)
- K-Java: A Complete Semantics of Java
- Denis Bogdanas and Grigore Rosu
POPL'15, ACM, pp 445-456. 2015
PDF, Slides(PDF), K-Java, DOI, POPL'15, BIB- All-Path Reachability Logic
- Andrei Stefanescu and Stefan Ciobaca and Radu Mereuta and Brandon Moore and Traian Florin Serbanuta and Grigore Rosu
RTA'14, LNCS 8560, pp 425-440. 2014
PDF, Slides(PPTX), Matching Logic, DOI, RTA'14, BIB- Matching Logic: A Logic for Structural Reasoning
- Grigore Rosu
Technical Report http://hdl.handle.net/2142/47004, Jan 2014
PDF, Matching Logic, DOI, BIB- The Rewriting Logic Semantics Project: A Progress Report
- Jose Meseguer and Grigore Rosu
Information and Computation, Volume 231(1), pp 38-69. 2013
PDF, K, DOI, Information and Computation, BIB- One-Path Reachability Logic
- Grigore Rosu and Andrei Stefanescu and Stefan Ciobaca and Brandon Moore
LICS'13, IEEE, pp 358-367. 2013
PDF, Slides(PPTX), Reachability Logic, LICS'13, BIB- Low-Level Program Verification using Matching Logic Reachability
- Dwight Guth and Andrei Stefanescu and Grigore Rosu
LOLA'13. 2013
PDF, Slides(PDF), Matching Logic, LOLA'13, BIB- Checking Reachability using Matching Logic
- Grigore Rosu and Andrei Stefanescu
OOPSLA'12, ACM, pp 555-574. 2012
PDF, Slides(PPTX), Slides(PDF), Matching Logic, DOI, OOPSLA'12, BIB- From Hoare Logic to Matching Logic Reachability
- Grigore Rosu and Andrei Stefanescu
FM'12, LNCS 7436, pp 387-402. 2012
PDF, Slides(PPTX), Slides(PDF), Matching Logic, DOI, FM'12, BIB- Towards a Unified Theory of Operational and Axiomatic Semantics
- Grigore Rosu and Andrei Stefanescu
ICALP'12, LNCS 7392, pp 351-363. 2012
PDF, Slides(PPTX), Slides(PDF), Matching Logic, DOI, ICALP'12, 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), Matching Logic, DOI, 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, 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
Links
matching logic at UIUC.
K framework webpage.
