# K and Matching Logic

(back to Grigore Rosu's webpage)

Would you like to wake up some morning, have a coffee, then design a non-trivial programming language, say with multidimensional arrays and array references, with functions and references to them, with blocks and local declarations, with input/output, with exceptions, with nondeterminism and concurrency with synchronization, and so on, and by evening to have a reasonably efficient interpreter, a state-space search tool and a model checker, as well as a deductive program verifier for your language, all correct-by-construction? Then you may be interested in K and Matching Logic, because that is what they are aiming for.

K is a rewrite-based framework for defining formal operational semantics of programming languages. A K semantics can be executed, and thus tested, as if it was an interpreter. This way, we can gain confidence in the correctness of our semantics. Then matching logic allows us to use precisely that semantics, unchanged, for program analysis and verification, without a need to give the language another, e.g., axiomatic or denotational or dynamic semantics. Matching logic consists of a language-independent proof system to reason about programs in any language that has a rewrite-based operational semantics. Although K and matching logic fit well together, they are researched independently, for the benefit of both. For example, the K tools focus on yielding efficient and realistic (e.g., interactive) interpreters, in addition to generating rewrite systems as needed for matching logic verification, while the matching logic verifiers focus on working with rewrite systems corresponding to any operational semantics style, not only to K definitions. Below are links to the two projects:

Movies, Interviews, Quick Overviews |
---|

- The Art and Science of Program Verification: Interview (on Channel 9) about K and matching logic (ICSE'11):
- Latest: PPTX PDF
- Status in October 2011: PPTX
- Status in August 2011: PPTX PDF

Select Publications |
---|

- The theoretical foundations of the K framework and a non-trivial language, CHALLENGE, defined in K:

*An Overview of the K Semantic Framework*- Grigore Rosu and Traian Florin Serbanuta
, Volume 79(6), pp 397-434. 2010**J.LAP**

PDF, Slides(PPTX), Slides(PDF), K Tool, J.LAP, BIB

- The theoretical foundations of matching logic and the implementation of MatchC:

*Checking Reachability using Matching Logic*- Grigore Rosu and Andrei Stefanescu
, ACM, pp 555-574. 2012**OOPSLA'12**

PDF, Slides(pptx), Slides(pdf), Matching Logic, OOPSLA'12, BIB

All Publications |
---|

Below we list all our publications related to K or Matching Logic, in reverse chronological order.

*A Truly Concurrent Semantics for the K Framework Based on Graph Transformations*- Traian Florin Serbanuta and Grigore Rosu
, LNCS 7562, pp 294-310. 2012**ICGT'12**

PDF, ICGT'12, Slides(PDF), BIB *Checking Reachability using Matching Logic*- Grigore Rosu and Andrei Stefanescu
, ACM, pp 555-574. 2012**OOPSLA'12**

PDF, Slides(pptx), Slides(pdf), Matching Logic, OOPSLA'12, BIB *Reachability Logic*- Grigore Rosu, Andrei Stefanescu, Stefan Ciobaca and Brandon Moore
http://hdl.handle.net/2142/32952, July 2012**Technical Report**

PDF, TR@UIUC *A Formal Semantics of C with Applications*- Chucky Ellison
, University of Illinois, July 2012**PhD Thesis**

PDF, Slides, Project, BIB *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, FM'12, SVN, BIB *Executing Formal Semantics with the K Tool*- David Lazar, Andrei Arusoaie, Traian Florin Serbanuta, Chucky Ellison, Radu Mereuta, Dorel Lucanu and Grigore Rosu
, LNCS 7436, pp 267-271. 2012**FM'12**

PDF, Slides(PDF), FM'12, DBLP, BIB *Towards a Unified Theory of Operational and Axiomatic Semantics*- Grigore Rosu and Andrei Stefanescu
, LNCS 7392, pp 351-363. 2012**ICALP'12**

PDF, Slides(pptx), Slides(pdf), Matching Logic, ICALP'12, BIB *Defining the Undefinedness of C*- Chucky Ellison and Grigore Rosu
http://hdl.handle.net/2142/30780, April 2012**Technical Report**

PDF, TR@UIUC, BIB *K Framework Distilled*- Dorel Lucanu, Traian Florin Serbanuta and Grigore Rosu
, LNCS 7571, pp 31-53. 2012**WRLA'12****Invited Paper**

PDF, Slides (PDF), WRLA'12, LNCS, BIB *Test-Case Reduction for C Compiler Bugs*- John Regehr, Yang Chen, Pascal Cuoq, Eric Eide, Chucky Ellison and Xuejun Yang
, ACM, pp 335-346. 2012**PLDI'12**

PDF, Slides(PPT), Project, ACM, PLDI'12, DBLP, BIB *The K Primer (version 2.5)*- Traian Florin Serbanuta, Andrei Arusoaie, David Lazar, Chucky Ellison, Dorel Lucanu and Grigore Rosu
, January 2012**Technical Report**

PDF, K 2.5, BIB *Making Maude Definitions more Interactive*- Andrei Arusoaie, Traian Florin Serbanuta, Chucky Ellison and Grigore Rosu
, LNCS 7571. 2012**WRLA'12**

PDF, Slides (PDF), WRLA'12, BIB *An Executable Formal Semantics of C with Applications*- Chucky Ellison and Grigore Rosu
, ACM, pp 533-544. 2012**POPL'12**

PDF, Slides(PDF), Project, ACM, POPL'12, DBLP, BIB *Matching Logic Rewriting: Unifying Operational and Axiomatic Semantics in a Practical and Generic Framework*- Grigore Rosu and Andrei Stefanescu
http://hdl.handle.net/2142/28357, November 2011**Technical Report**

PDF, Matching Logic, TR@UIUC, SVN, BIB *The Rewriting Logic Semantics Project: A Progress Report*- Jose Meseguer and Grigore Rosu
, LNCS 6914, pp 1-37. Invited talk. 2011**FCT'11**

PDF, K Tool, FCT'11, BIB *Matching Logic: A New Program Verification Approach (NIER Track)*- Grigore Rosu and Andrei Stefanescu
, ACM, pp. 868-871. 2011**ICSE'11**

PDF, Slides(pptx), Slides(pdf), Poster(pptx), Poster(pdf), Matching Logic, ACM, NIER ICSE'11, BIB *On Compiling Rewriting Logic Language Definitions into Competitive Interpreters*- Michael Ilseman, Chucky Ellison and Grigore Rosu
http://hdl.handle.net/2142/17444, December 2010**Technical Report**

PDF, TR@UIUC, Compiler Webpage, BIB *A Rewriting Approach to Concurrent Programming Language Design and Semantics*- Traian Florin Serbanuta
, University of Illinois, December 2010**PhD Thesis**

PDF, Slides (PDF), K-Maude, TR@UIUC, BIB *Matching Logic: A New Program Verification Approach*- Grigore Rosu and Andrei Stefanescu
. 2010**UV'10**

PDF, Slides(pptx), Slides(pdf), Matching Logic, K framework, UV'10, BIB *A Formal Executable Semantics of Verilog*- Patrick Meredith, Michael Katelman, Jose Meseguer and Grigore Rosu
http://hdl.handle.net/2142/17079, July 2010**Technical Report**

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

PDF, Slides(PPT), Slides(PDF), LNCS, AMAST'10, BIB *K-Maude: A Rewriting Based Tool for Semantics of Programming Languages*- Traian Florin Serbanuta and Grigore Rosu
, LNCS 6381, pp 104-122. 2010**WRLA'10**

PDF, Slides (PDF), K-Maude, LNCS, WRLA'10, BIB *Ambient intelligence in self-organising assembly systems using the chemical reaction model*- Regina Frei, Giovanna Di Marzo Serugendo and Traian Florin Serbanuta
, Volume 1(3), pp 163-184. 2010**J. of Ambient Intelligence and Humanized Computing**

J.AIHC, BIB *An Overview of the K Semantic Framework*- Grigore Rosu and Traian Florin Serbanuta
, Volume 79(6), pp 397-434. 2010**J.LAP**

PDF, Slides(PPTX), Slides(PDF), K Tool, J.LAP, BIB *A Formal Executable Semantics of Verilog*- Patrick Meredith, Michael Katelman, Jose Meseguer and Grigore Rosu
, IEEE, pp 179-188. 2010**MEMOCODE'10**

PDF, Slides(PDF), Sources, Verilog Semantics, IEEE, MEMOCODE'10, BIB *A Rewriting Logic Approach to Type Inference*- Chucky Ellison, Traian Florin Serbanuta and Grigore Rosu
, LNCS 5486, pp 135-151. 2009**WADT'08**

PDF, Slides(PDF), LNCS, WADT'08, BIB *Runtime Verification of C Memory Safety*- Grigore Rosu, Wolfram Schulte and Traian Florin Serbanuta
, LNCS 5779, pp 132-151. 2009**RV'09**

PDF, Slides (PDF), LNCS, RV'09, BIB *From Rewriting Logic Executable Semantics to Matching Logic Program Verification*- Grigore Rosu, Chucky Ellison and Wolfram Schulte
http://hdl.handle.net/2142/13159, July 2009**Technical Report**

PDF, TR@UIUC, BIB *Matching Logic --- Extended Report*- Grigore Rosu and Wolfram Schulte
UIUCDCS-R-2009-3026, January 2009**Technical Report**

TR@UIUC, BIB *Towards a Module System for K*- Mark Hills and Grigore Rosu
, LNCS 5486, pp 187-205. 2009**WADT'08**

PDF, LNCS, WADT'08, BIB *Deﬁning and Executing P-systems with Structured Data in K*- Traian Florin Serbanuta, Gheorghe Stefanescu and Grigore Rosu
, LNCS 5391, pp 374-393. 2009**WMC'08**

PDF, Slides (PDF), Experiments, LNCS, WMC'08, BIB *A Rewriting Logic Approach to Static Checking of Units of Measurement in C*- Mark Hills, Feng Chen and Grigore Rosu
, ENTCS, to appear, 2008**RULE'08**

PDF, RULE'08 slides, RULE'08, BIB *A Rewriting Logic Approach to Defining Type Systems*- Chucky Ellison
**Master's Thesis**

PDF, TR@UIUC, BIB *A Rewriting Logic Approach to Type Inference*- Chucky Ellison, Traian Florin Serbanuta and Grigore Rosu
UIUCDCS-R-2008-2934, March 2008**Technical report**

PDF, TR@UIUC, BIB *Memory Representations in Rewriting Logic Semantics Definitions*- Mark Hills
, ENTCS, to appear, 2008**WRLA'08**

PDF, WRLA'08 slides, WRLA'08, BIB *K: A Rewriting-Based Framework for Computations -- Preliminary version*- Grigore Rosu
UIUCDCS-R-2007-2926 and UILU-ENG-2007-1827, December 2007**Technical report**

PDF, ZIP, TR@UIUC, BIB *A K Definition of Scheme*- Patrick Meredith, Mark Hills and Grigore Rosu
UIUCDCS-R-2007-2907, October 2007**Technical Report**

PDF, TR@UIUC, BIB *An Executable Rewriting Logic Semantics of K-Scheme*- Patrick Meredith, Mark Hills and Grigore Rosu
, Technical Report DIUL-RT-0701, pp. 91-103, September 2007**8th Workshop on Scheme and Functional Programming**

PDF, SCHEME'07, BIB *A Rewriting Approach to the Design and Evolution of Object-Oriented Languages*- Mark Hills and Grigore Rosu
, ACM Press, pp 827-828. 2007**OOPSLA'07 Companion**

PDF, OOPSLA'07 poster, ACM, OOPSLA'07, BIB *A Rewriting Approach to the Design and Evolution of Object-Oriented Languages*- Mark Hills and Grigore Rosu
Bericht-Nr. 2007-7, pp. 23-26, July 2007**Technical Report**

PDF, ECOOP'07 Doctoral Symposium slides, ECOOP'07 Doctoral Symposium, BIB *A Rewrite Framework for Language Definitions and for Generation of Efficient Interpreters*- Mark Hills, Traian Florin Serbanuta and Grigore Rosu
, ENTCS 176(4), pp. 215-231. 2007**WRLA'06**

PDF, Experiments, ENTCS, WRLA'06, BIB *K: a Rewrite-based Framework for Modular Language Design, Semantics, Analysis and Implementation*- Grigore Rosu
UIUCDCS-R-2006-2802, December 2006**Technical report**

PDF, TR@UIUC, BIB *Rewriting Logic Semantics: From Language Specifications to Formal Analysis Tools*- Jose Meseguer and Grigore Rosu
, LNCS 3097, pp 1-44. 2004**IJCAR'04**

PDF, Maude-code, LNCS, IJCAR'04, BIB *Formal Analysis of Java Programs in JavaFAN*- Azadeh Farzan, Feng Chen, Jose Meseguer and Grigore Rosu
, LNCS 3114, pp 501 - 505. 2004.**CAV'04**

PDF, LNCS, CAV'04, DBLP, BIB *CS322 - Programming Language Design: Lecture Notes*- Grigore Rosu
UIUCDCS-R-2003-2897, December 2003**Technical Report**

PDF, TR @ UIUC, BIB