# 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:

- The most recent indepth presentation of the mathematical foundations of matching logic.

*Matching logic*- Grigore Rosu
, Volume 13(4), pp 1-61. 2017**LMCS**

PDF, project, DOI, LMCS, BIB

- 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
, LNCS 8560, pp 425-440. 2014**RTA'14**

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
, IEEE, pp 358-367. 2013**LICS'13**

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
, ACM, pp 555-574. 2012**OOPSLA'12**

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
, LNCS 7436, pp 387-402. 2012**FM'12**

PDF, Slides(PPTX), Slides(PDF), Matching Logic, DOI, FM'12, BIB

## Other

### Older slides

### Old implementations

### Complete list of Publications (reverse chronological order)

Program Verification by Coinduction- Brandon Moore and Lucas Pena and Grigore Rosu
, Springer, pp 589-618. 2018ESOP'18

PDF, Matching Logic, DOI, ESOP'18, BIBMatching logic- Grigore Rosu
, Volume 13(4), pp 1-61. 2017LMCS

PDF, project, DOI, LMCS, BIBK - A Semantic Framework for Programming Languages and Formal Analysis Tools- Grigore Rosu

, NATO Science for Peace and Security. 2017. To appearMarktoberdorf'16

PDF, K, BIBSemantics-Based Program Verifiers for All Languages- Andrei Stefanescu and Daejun Park and Shijiao Yuwen and Yilong Li and Grigore Rosu
, ACM, pp 74-91. 2016OOPSLA'16

PDF, Slides(PDF), Matching Logic, DOI, OOPSLA'16, BIBFinite-Trace Linear Temporal Logic: Coinductive Completeness- Grigore Rosu
, LNCS 10012, pp 333-350. 2016RV'16

PDF, Slides(PPTX), Matching Logic, DOI, RV'16, BIBRV-Match: Practical Semantics-Based Program Analysis- Dwight Guth and Chris Hathhorn and Manasvi Saxena and Grigore Rosu
, LNCS 9779, pp 447-453. 2016CAV'16

PDF, RV-Match, DOI, CAV'16, BIBA Language-Independent Proof System for Full Program Equivalence- Stefan Ciobaca and Dorel Lucanu and Vlad Rusu and Grigore Rosu
, Volume 28(3), pp 469-497. 2016J.FAOC

PDF, Matching Logic, DOI, J.FAOC, BIBTowards a Kool Future- Dorel Lucanu and Traian Florin Serbanuta and Grigore Rosu
, LNCS 9660, pp 325-343. 2016Boer's Festschrift

PDF, K, DOI, Boer's Festschrift, BIBFrom Rewriting Logic, to Programming Language Semantics, to Program Verification- Grigore Rosu
, LNCS 9200, pp 598-616. 2015Meseguer's Festschrift

PDF, Slides(PPTX), K, DOI, Meseguer's Festschrift, BIBMatching Logic --- Extended Abstract- Grigore Rosu
, Leibniz International Proceedings in Informatics (LIPIcs) 36, pp 5-21. 2015RTA'15

PDF, Slides(PPTX), Matching Logic, DOI, RTA'15, BIBProgram Verification by Coinduction- Brandon Moore and Grigore Rosu
http://hdl.handle.net/2142/73177, February 2015Technical Report

PDF, Matching Logic, DOI, BIBK-Java: A Complete Semantics of Java- Denis Bogdanas and Grigore Rosu
, ACM, pp 445-456. 2015POPL'15

PDF, Slides(PDF), K-Java, DOI, POPL'15, BIBA Language-Independent Proof System for Mutual Program Equivalence- Stefan Ciobaca and Dorel Lucanu and Vlad Rusu and Grigore Rosu
, LNCS 8829, pp 75-90. 2014ICFEM'14

PDF, Slides(PDF), Matching Logic, DOI, ICFEM'14, BIBAll-Path Reachability Logic- Andrei Stefanescu and Stefan Ciobaca and Radu Mereuta and Brandon Moore and Traian Florin Serbanuta and Grigore Rosu
, LNCS 8560, pp 425-440. 2014RTA'14

PDF, Slides(PPTX), Matching Logic, DOI, RTA'14, BIBMatching Logic: A Logic for Structural Reasoning- Grigore Rosu
http://hdl.handle.net/2142/47004, Jan 2014Technical Report

PDF, Matching Logic, DOI, BIBThe Rewriting Logic Semantics Project: A Progress Report- Jose Meseguer and Grigore Rosu
, Volume 231(1), pp 38-69. 2013Information and Computation

PDF, K, DOI, Information and Computation, BIBOne-Path Reachability Logic- Grigore Rosu and Andrei Stefanescu and Stefan Ciobaca and Brandon Moore
, IEEE, pp 358-367. 2013LICS'13

PDF, Slides(PPTX), Reachability Logic, LICS'13, BIBLow-Level Program Verification using Matching Logic Reachability- Dwight Guth and Andrei Stefanescu and Grigore Rosu
. 2013LOLA'13

PDF, Slides(PDF), Matching Logic, LOLA'13, BIBChecking Reachability using Matching Logic- Grigore Rosu and Andrei Stefanescu
, ACM, pp 555-574. 2012OOPSLA'12

PDF, Slides(PPTX), Slides(PDF), Matching Logic, DOI, OOPSLA'12, BIBFrom Hoare Logic to Matching Logic Reachability- Grigore Rosu and Andrei Stefanescu
, LNCS 7436, pp 387-402. 2012FM'12

PDF, Slides(PPTX), Slides(PDF), Matching Logic, DOI, FM'12, BIBReachability Logic- Grigore Rosu and Andrei Stefanescu and Stefan Ciobaca and Brandon Moore
http://hdl.handle.net/2142/32952, Jul 2012Technical Report

PDF, Reachability Logic, DOI, BIBTowards a Unified Theory of Operational and Axiomatic Semantics- Grigore Rosu and Andrei Stefanescu
, LNCS 7392, pp 351-363. 2012ICALP'12

PDF, Slides(PPTX), Slides(PDF), Matching Logic, DOI, ICALP'12, BIBMatchC: A Matching Logic Reachability Verifier Using the K Framework- Andrei Stefanescu
, ENTCS 304. 2011K'11

PDF, Matching Logic, DOI, BIBThe Rewriting Logic Semantics Project: A Progress Report- Jose Meseguer and Grigore Rosu
, Lecture Notes in Computer Science 6914, pp 1-37. 2011FCT'11

PDF, K, DOI, FCT'11, BIBTowards Semantics-Based WCET Analysis- Mihail Asavoae and Dorel Lucanu and Grigore Rosu
. 2011WCET'11

PDF, Slides(PDF), Matching Logic, WCET'11, BIBMatching Logic: A New Program Verification Approach (NIER Track)- Grigore Rosu and Andrei Stefanescu
, ACM, pp 868-871. 2011ICSE'11

PDF, Slides(PPTX), Slides(PDF), Matching Logic, DOI, ICSE'11, BIBMatching Logic: A New Program Verification Approach- Grigore Rosu and Andrei Stefanescu
. 2010UV'10

Slides(PPTX), Slides(PDF), Matching Logic, UV'10Matching Logic: An Alternative to Hoare/Floyd Logic- Grigore Rosu and Chucky Ellison and Wolfram Schulte
, Springer, pp 142-162. 2010AMAST'10

PDF, Slides(PPTX), Slides(PDF), Matching Logic, DOI, AMAST'10, BIBMatching Logic --- Extended Report- Grigore Rosu and Wolfram Schulte
http://hdl.handle.net/2142/10790, January 2009Technical Report

PDF, Matching Logic, DOI, BIBCS322 - Programming Language Design: Lecture Notes- Grigore Rosu
http://hdl.handle.net/2142/11385, December 2003Technical Report

PDF, Matching Logic, DOI, BIB

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

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

### Links

matching logic at UIUC.

K framework webpage.