# Programming Language Design and Semantics

(back to Grigore Rosu's webpage)

Introduction and Motivation |
---|

Unlike natural language, which allows interpretation and miscommunication, programming languages are meant to tell computers *precisely* what to do.
Without a rigorous definition of a programming language that unambiguously says what each program does, it is impossible to guarantee reliable, safe or secure operation of computers.
We firmly believe in the *ideal language framework* approach, where each programming language has a formal definition and then the various tools for that language are derived automatically, at no additional effort specific to that language.
This is illustrated in the picture to the right.
The framework (meta-)language used for formally defining programming languages must be:
*user-friendly*, so language designers use it as a natural means to create and experiment with their languages;
*mathematically rigorous*, so the resulting language definitions can be used as a basis for formal reasoning about programs;
*modular*, so the defined languages are easy to extend with new features without having to revisit already defined features;
and *expressive*, so we can define any programming language with arbitrarily complex features.
The generic tools instantiated for any given language must be *correct-by-construction*, so we can trust their results, and *efficient*, so there is no need for wasting time and energy to implement language-specific tools.

If you are new to the programming language foundations field, you are probably asking yourself *"Why would it be any other way?"*.
If you are theoretically inclined, you are probably thinking *"Isn't it obvious that once I have a language definition giving a transition system for any program, that generic tools for transition systems can be used to obtain specialized tools for my language?"*.
We agree.
Unfortunately and almost unbelievably after half a century of research in this area, the state-of-the-art in programming languages (as of 2016) is still to have no formal definition of the programming language, or to define a language by an adhoc untrusted translation to another language which may itself have no formal definition, and then each tool to implement its own projection of a hypothetical model of the language at the discretion of its developers, and the same tool for different languages, say a model checker, to re-implement the same algorithms and abstractions slightly adapted to each target language.
And ironically, the resulting tool is then called a "formal analysis tool" or a "program verifier" for that language, and used to verify and validate safety critical software upon which our lives depend.
We believe we should put a stop to this and do things right.
We know the ideal framework approach is possible and is practical.
We are pursuing it.
Below we detail our approach, provide reading material, address FAQs, and list several open problems and challenges.

K and Matching Logic |
---|

We are developing the K framework, an implementation of matching logic, whose design and development are driven by the ideal language framework belief above. The commercial tool RV-Match builds upon K using an efficient execution engine and a comprehensive semantics of C. K provides a user-friendly rewrite-based language for defining formal operational semantics of programming languages. A K language semantics can be executed, and thus tested, as if it were an interpreter. A generic matching logic reasoning engine allows you to use the K language semantics for symbolic execution and various kinds of program analysis and verification, without a need to give the language any other (axiomatic or denotational or dynamic, etc.) semantics. Matching logic consists of a fixed proof system to reason about programs in any language defined with 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:

Below is a list of frequently asked questions. You may want to check these even if you do not have any question to ask, because our answers often include historical remarks, make connections, clarify misunderstandings/misconceptions, and suggest reading material that you may find useful.

If the above sounds interesting to you and would like to join our effort, please check these out (look for the problems tagged with PL):

Select Publications |
---|

- High-level overview of our PL design, semantics and verification approach:

*From Rewriting Logic, to Programming Language Semantics, to Program Verification*- Grigore Rosu
, LNCS 9200, pp 598-616. 2015**Meseguer's Festschrift**

PDF, Slides(PPTX), K, DOI, Meseguer's Festschrift, BIB

- Overview of K and a non-trivial example language definition:

*K Overview and SIMPLE Case Study*- Grigore Rosu and Traian Florin Serbanuta
, ENTCS 304, pp 3-56. 2014**K'11**

PDF, K, DOI, K'11, BIB

- The theoretical foundations of the K framework and a tricky 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.

*Connecting Constrained Constructor Patterns and Matching Logic*- Xiaohong Chen and Dorel Lucanu and Grigore Rosu

. 2020. To appear**WRLA'20**

PDF, Matching Logic, WRLA'20, BIB *A General Approach to Define Binders Using Matching Logic*- Xiaohong Chen and Grigore Rosu

http://hdl.handle.net/2142/106608, March 2020**Technical Report**

PDF, Matching Logic, DOI, BIB *Applicative Matching Logic: Semantics of K*- Xiaohong Chen and Grigore Rosu
http://hdl.handle.net/2142/104616, July 2019**Technical Report**

PDF, Matching Logic, DOI, BIB *A Complete Formal Semantics of x86-64 User-Level Instruction Set Architecture*- Sandeep Dasgupta and Daejun Park and Theodoros Kasampalis and Vikram S. Adve and Grigore Rosu
, ACM, pp 1133-1148. 2019**PLDI'19**

PDF, Slides(PDF), Semantics, DOI, PLDI'19, BIB *Matching mu-Logic*- Xiaohong Chen and Grigore Rosu
, ACM/IEEE, pp 1-13. 2019**LICS'19**

PDF, Slides(PPTX), Matching Logic, DOI, LICS'19, BIB *Matching mu-Logic: Foundation of K Framework*- Xiaohong Chen and Grigore Rosu
, Leibniz International Proceedings in Informatics (LIPIcs) 139, pp 1-4. 2019**CALCO'19**

PDF, Slides(PPTX), Matching Logic, DOI, CALCO'19, BIB *Matching mu-Logic*- Xiaohong Chen and Grigore Rosu
http://hdl.handle.net/2142/102281, January 2019**Technical Report**

PDF, Matching Logic, DOI, BIB *SETSS'19 Lecture Notes on K*- Xiaohong Chen and Grigore Rosu

, Lecture Notes in Computer Science. 2019. To appear**SETSS'19**

PDF, Slides(PPTX), K, BIB *A Language-Independent Program Verification Framework*- Xiaohong Chen and Grigore Rosu
, Springer, pp 92-102. 2018**ISoLA'18**

PDF, Slides(PPTX), DOI, ISoLA'18, BIB *A Language-Independent Approach to Smart Contract Verification*- Xiaohong Chen and Daejun Park and Grigore Rosu
, Springer, pp 405-413. 2018**ISoLA'18**

PDF, Slides(PPTX), Formally Verified Smart Contracts, DOI, ISoLA'18, BIB *A Formal Verification Tool for Ethereum VM Bytecode*- Daejun Park and Yi Zhang and Manasvi Saxena and Philip Daian and Grigore Rosu
, ACM, pp 912-915. 2018**ESEC/FSE'18**

PDF, Slides(PDF), Formally Verified Smart Contracts, DOI, ESEC/FSE'18, BIB *IELE: An Intermediate-Level Blockchain Language Designed and Implemented Using Formal Semantics*- Theodoros Kasampalis and Dwight Guth and Brandon Moore and Traian Serbanuta and Virgil Serbanuta and Daniele Filaretti and Grigore Rosu and Ralph Johnson
http://hdl.handle.net/2142/100320, July 2018**Technical Report**

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

PDF, Matching Logic, DOI, ESOP'18, BIB *P4K: A Formal Semantics of P4 and Applications*- Ali Kheradmand and Grigore Rosu
https://arxiv.org/abs/1804.01468, April 2018**Technical Report**

PDF, P4K, DOI, BIB *KEVM: A Complete Semantics of the Ethereum Virtual Machine*- Everett Hildenbrandt and Manasvi Saxena and Xiaoran Zhu and Nishant Rodrigues and Philip Daian and Dwight Guth and Brandon Moore and Yi Zhang and Daejun Park and Andrei Stefanescu and Grigore Rosu
, IEEE, pp 204-217. 2018**CSF 2018**

PDF, KEVM, CSF 2018, BIB *Matching logic*- Grigore Rosu
, Volume 13(4), pp 1-61. 2017**LMCS**

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

, NATO Science for Peace and Security. 2017. To appear**Marktoberdorf'16**

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

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

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

PDF, RV-Match, DOI, CAV'16, BIB *A 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. 2016**J.FAOC**

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

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

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

PDF, Slides(PPTX), Matching Logic, DOI, RTA'15, BIB *Defining the Undefinedness of C*- Chris Hathhorn and Chucky Ellison and Grigore Rosu
, ACM, pp 336-345. 2015**PLDI'15**

PDF, C Semantics, DOI, PLDI'15, BIB *KJS: A Complete Formal Semantics of JavaScript*- Daejun Park and Andrei Stefanescu and Grigore Rosu
, ACM, pp 346-356. 2015**PLDI'15**

PDF, Slides(PDF), Semantics, DOI, PLDI'15, BIB *Program Verification by Coinduction*- Brandon Moore and Grigore Rosu
http://hdl.handle.net/2142/73177, February 2015**Technical Report**

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

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

PDF, Slides(PDF), Matching Logic, DOI, ICFEM'14, BIB *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 *K Overview and SIMPLE Case Study*- Grigore Rosu and Traian Florin Serbanuta
, ENTCS 304, pp 3-56. 2014**K'11**

PDF, K, DOI, K'11, BIB *Abstract Semantics for K Module Composition*- Codruta Girlea and Grigore Rosu
, ENTCS 304, pp 127-149. 2014**K'11**

PDF, K, DOI, K'11, BIB *The K Primer (version 3.3)*- Traian Florin Serbanuta and Andrei Arusoaie and David Lazar and Chucky Ellison and Dorel Lucanu and Grigore Rosu
, ENTCS 304, pp 57-80. 2014**K'11**

PDF, K, DOI, K'11, BIB *Matching Logic: A Logic for Structural Reasoning*- Grigore Rosu
http://hdl.handle.net/2142/47004, Jan 2014**Technical Report**

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

PDF, K, DOI, Information and Computation, BIB *Specifying Languages and Verifying Programs with K*- Grigore Rosu
, IEEE/CPS, pp 28-31. 2013**SYNASC'13**

PDF, Slides(PPTX), K, DOI, SYNASC'13, BIB *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 *Low-Level Program Verification using Matching Logic Reachability*- Dwight Guth and Andrei Stefanescu and Grigore Rosu
. 2013**LOLA'13**

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

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

PDF, Reachability Logic, DOI, 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, DOI, ICALP'12, BIB *Defining the Undefinedness of C*- Chucky Ellison and Grigore Rosu
http://hdl.handle.net/2142/30780, April 2012**Technical Report**

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

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

PDF, K, DOI, 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), Semantics, DOI, POPL'12, BIB *MatchC: A Matching Logic Reachability Verifier Using the K Framework*- Andrei Stefanescu
, ENTCS 304. 2011**K'11**

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

PDF, K, DOI, FCT'11, BIB *An Executable Formal Semantics of C with Applications*- Chucky Ellison and Grigore Rosu
http://hdl.handle.net/2142/25816, July 2011**Technical Report**

PDF, C Semantics, DOI, BIB *Towards Semantics-Based WCET Analysis*- Mihail Asavoae and Dorel Lucanu and Grigore Rosu
. 2011**WCET'11**

PDF, Slides(PDF), Matching Logic, WCET'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), Matching Logic, DOI, ICSE'11, BIB *A Formal Semantics of C with Applications*- Chucky Ellison and Grigore Rosu
http://hdl.handle.net/2142/17414, November 2010**Technical Report**

PDF, C Semantics, DOI, BIB *Matching Logic: A New Program Verification Approach*- Grigore Rosu and Andrei Stefanescu
. 2010**UV'10**

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

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

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

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

PDF, Matching Logic, DOI, BIB

*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, , 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, , 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