Programming Language Design and Semantics

From FSL
(Redirected from K and Matching Logic)
Jump to: navigation, search

(back to Grigore Rosu's webpage)


Introduction and Motivation
Ideal language framework: tools derived from formal language definition.

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:

K Framework
Matching Logic

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.

FAQs

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

Open Problems and Challenges


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
Meseguer's Festschrift, LNCS 9200, pp 598-616. 2015
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
K'11, ENTCS 304, pp 3-56. 2014
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
J.LAP, Volume 79(6), pp 397-434. 2010
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
OOPSLA'12, ACM, pp 555-574. 2012
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.

Towards a Kool Future 
Dorel Lucanu and Traian Florin Serbanuta and Grigore Rosu
Boer's Festschrift, LNCS 9660, pp 325-343. 2016
PDF, K, DOI, Boer's Festschrift, BIB
A Language-Independent Proof System for Full Program Equivalence 
Stefan Ciobaca and Dorel Lucanu and Vlad Rusu and Grigore Rosu
J.FAOC. 2016
PDF, Matching Logic, DOI, J.FAOC, BIB
From Rewriting Logic, to Programming Language Semantics, to Program Verification 
Grigore Rosu
Meseguer's Festschrift, LNCS 9200, pp 598-616. 2015
PDF, Slides(PPTX), K, DOI, Meseguer's Festschrift, BIB
Matching Logic --- Extended Abstract 
Grigore Rosu
RTA'15, Leibniz International Proceedings in Informatics (LIPIcs) 36, pp 5-21. 2015
PDF, Slides(PPTX), Matching Logic, DOI, RTA'15, BIB
Defining the Undefinedness of C 
Chris Hathhorn and Chucky Ellison and Grigore Rosu
PLDI'15, ACM, pp 336-345. 2015
PDF, C Semantics, DOI, PLDI'15, BIB
KJS: A Complete Formal Semantics of JavaScript 
Daejun Park and Andrei Stefanescu and Grigore Rosu
PLDI'15, ACM, pp 346-356. 2015
PDF, Slides(PDF), Semantics, DOI, PLDI'15, BIB
Program Verification by Coinduction 
Brandon Moore and Grigore Rosu
Technical Report http://hdl.handle.net/2142/73177, February 2015
PDF, Matching Logic, DOI, BIB
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
A Language-Independent Proof System for Mutual Program Equivalence 
Stefan Ciobaca and Dorel Lucanu and Vlad Rusu and Grigore Rosu
ICFEM'14, LNCS 8829, pp 75-90. 2014
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
RTA'14, LNCS 8560, pp 425-440. 2014
PDF, Slides(PPTX), Matching Logic, DOI, RTA'14, BIB
K Overview and SIMPLE Case Study 
Grigore Rosu and Traian Florin Serbanuta
K'11, ENTCS 304, pp 3-56. 2014
PDF, K, DOI, K'11, BIB
Abstract Semantics for K Module Composition 
Codruta Girlea and Grigore Rosu
K'11, ENTCS 304, pp 127-149. 2014
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
K'11, ENTCS 304, pp 57-80. 2014
PDF, K, DOI, K'11, 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
Specifying Languages and Verifying Programs with K 
Grigore Rosu
SYNASC'13, IEEE/CPS, pp 28-31. 2013
PDF, Slides(PPTX), K, DOI, SYNASC'13, 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
A Truly Concurrent Semantics for the K Framework Based on Graph Transformations 
Traian Florin Serbanuta and Grigore Rosu
ICGT'12, LNCS 7562, pp 294-310. 2012
PDF, Slides(PDF), K, DOI, ICGT'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
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
FM'12, LNCS 7436, pp 267-271. 2012
PDF, Slides(PDF), K, DOI, FM'12, BIB
Reachability Logic 
Grigore Rosu and Andrei Stefanescu and Stefan Ciobaca and Brandon Moore
Technical Report http://hdl.handle.net/2142/32952, Jul 2012
PDF, Reachability Logic, DOI, 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
Defining the Undefinedness of C 
Chucky Ellison and Grigore Rosu
Technical Report http://hdl.handle.net/2142/30780, April 2012
PDF, K, DOI, BIB
Making Maude Definitions more Interactive 
Andrei Arusoaie and Traian Florin Serbanuta and Chucky Ellison and Grigore Rosu
WRLA'12, LNCS 7571, pp 83-98. 2012
PDF, K, DOI, WRLA'12, BIB
K Framework Distilled 
Dorel Lucanu and Traian Florin Serbanuta and Grigore Rosu
WRLA'12, LNCS 7571, pp 31-53. 2012
PDF, K, DOI, WRLA'12, BIB
An Executable Formal Semantics of C with Applications 
Chucky Ellison and Grigore Rosu
POPL'12, ACM, pp 533-544. 2012
PDF, Slides(PDF), Semantics, DOI, POPL'12, BIB
MatchC: A Matching Logic Reachability Verifier Using the K Framework 
Andrei Stefanescu
K'11, ENTCS 304. 2011
PDF, Matching Logic, DOI, BIB
The Rewriting Logic Semantics Project: A Progress Report 
Jose Meseguer and Grigore Rosu
FCT'11, Lecture Notes in Computer Science 6914, pp 1-37. 2011
PDF, K, DOI, FCT'11, BIB
An Executable Formal Semantics of C with Applications 
Chucky Ellison and Grigore Rosu
Technical Report http://hdl.handle.net/2142/25816, July 2011
PDF, C Semantics, DOI, BIB
Towards Semantics-Based WCET Analysis 
Mihail Asavoae and Dorel Lucanu and Grigore Rosu
WCET'11. 2011
PDF, Slides(PDF), Matching Logic, WCET'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), Matching Logic, DOI, ICSE'11, BIB
A Formal Semantics of C with Applications 
Chucky Ellison and Grigore Rosu
Technical Report http://hdl.handle.net/2142/17414, November 2010
PDF, C Semantics, DOI, BIB
Matching Logic: A New Program Verification Approach 
Grigore Rosu and Andrei Stefanescu
UV'10. 2010
Slides(PPTX), Slides(PDF), Matching Logic, UV'10
Matching Logic: An Alternative to Hoare/Floyd Logic 
Grigore Rosu and Chucky Ellison and Wolfram Schulte
AMAST'10, Springer, pp 142-162. 2010
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
WRLA'10, Springer, pp 104-122. 2010
PDF, Slides(PDF), K, DOI, WRLA'10, BIB
Matching Logic --- Extended Report 
Grigore Rosu and Wolfram Schulte
Technical Report http://hdl.handle.net/2142/10790, January 2009
PDF, Matching Logic, DOI, BIB
CS322 - Programming Language Design: Lecture Notes 
Grigore Rosu
Technical Report http://hdl.handle.net/2142/11385, December 2003
PDF, Matching Logic, DOI, BIB



A Truly Concurrent Semantics for the K Framework Based on Graph Transformations 
Traian Florin Serbanuta and Grigore Rosu
ICGT'12, LNCS 7562, pp 294-310. 2012
PDF, ICGT'12, Slides(PDF), 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, OOPSLA'12, BIB
Reachability Logic 
Grigore Rosu, Andrei Stefanescu, Stefan Ciobaca and Brandon Moore
Technical Report http://hdl.handle.net/2142/32952, July 2012
PDF, TR@UIUC
A Formal Semantics of C with Applications 
Chucky Ellison
PhD Thesis, University of Illinois, July 2012
PDF, Slides, Project, 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, 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
FM'12, LNCS 7436, pp 267-271. 2012
PDF, Slides(PDF), FM'12, DBLP, 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, ICALP'12, BIB
Defining the Undefinedness of C 
Chucky Ellison and Grigore Rosu
Technical Report http://hdl.handle.net/2142/30780, April 2012
PDF, TR@UIUC, BIB
K Framework Distilled 
Dorel Lucanu, Traian Florin Serbanuta and Grigore Rosu
WRLA'12, LNCS 7571, pp 31-53. 2012 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
PLDI'12, ACM, pp 335-346. 2012
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
Technical Report, January 2012
PDF, K 2.5, BIB
Making Maude Definitions more Interactive 
Andrei Arusoaie, Traian Florin Serbanuta, Chucky Ellison and Grigore Rosu
WRLA'12, LNCS 7571. 2012
PDF, Slides (PDF), WRLA'12, BIB
An Executable Formal Semantics of C with Applications 
Chucky Ellison and Grigore Rosu
POPL'12, ACM, pp 533-544. 2012
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
Technical Report http://hdl.handle.net/2142/28357, November 2011
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
On Compiling Rewriting Logic Language Definitions into Competitive Interpreters 
Michael Ilseman, Chucky Ellison and Grigore Rosu
Technical Report http://hdl.handle.net/2142/17444, December 2010
PDF, TR@UIUC, Compiler Webpage, BIB
A Rewriting Approach to Concurrent Programming Language Design and Semantics 
Traian Florin Serbanuta
PhD Thesis, University of Illinois, December 2010
PDF, Slides (PDF), K-Maude, TR@UIUC, 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
A Formal Executable Semantics of Verilog 
Patrick Meredith, Michael Katelman, Jose Meseguer and Grigore Rosu
Technical Report http://hdl.handle.net/2142/17079, July 2010
PDF, TR@UIUC, 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
K-Maude: A Rewriting Based Tool for Semantics of Programming Languages 
Traian Florin Serbanuta and Grigore Rosu
WRLA'10, LNCS 6381, pp 104-122. 2010
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
J. of Ambient Intelligence and Humanized Computing, Volume 1(3), pp 163-184. 2010
J.AIHC, BIB
An Overview of the K Semantic Framework 
Grigore Rosu and Traian Florin Serbanuta
J.LAP, Volume 79(6), pp 397-434. 2010
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
MEMOCODE'10, IEEE, pp 179-188. 2010
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
WADT'08, LNCS 5486, pp 135-151. 2009
PDF, Slides(PDF), LNCS, WADT'08, BIB
Runtime Verification of C Memory Safety 
Grigore Rosu, Wolfram Schulte and Traian Florin Serbanuta
RV'09, LNCS 5779, pp 132-151. 2009
PDF, Slides (PDF), LNCS, RV'09, 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
Towards a Module System for K 
Mark Hills and Grigore Rosu
WADT'08, LNCS 5486, pp 187-205. 2009
PDF, LNCS, WADT'08, BIB
Defining and Executing P-systems with Structured Data in K 
Traian Florin Serbanuta, Gheorghe Stefanescu and Grigore Rosu
WMC'08, LNCS 5391, pp 374-393. 2009
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
RULE'08, ENTCS, to appear, 2008
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
Technical report UIUCDCS-R-2008-2934, March 2008
PDF, TR@UIUC, BIB
Memory Representations in Rewriting Logic Semantics Definitions 
Mark Hills
WRLA'08, ENTCS, to appear, 2008
PDF, WRLA'08 slides, WRLA'08, BIB
K: A Rewriting-Based Framework for Computations -- Preliminary version 
Grigore Rosu
Technical report UIUCDCS-R-2007-2926 and UILU-ENG-2007-1827, December 2007
PDF, ZIP, TR@UIUC, BIB
A K Definition of Scheme 
Patrick Meredith, Mark Hills and Grigore Rosu
Technical Report UIUCDCS-R-2007-2907, October 2007
PDF, TR@UIUC, BIB
An Executable Rewriting Logic Semantics of K-Scheme 
Patrick Meredith, Mark Hills and Grigore Rosu
8th Workshop on Scheme and Functional Programming, Technical Report DIUL-RT-0701, pp. 91-103, September 2007
PDF, SCHEME'07, BIB
A Rewriting Approach to the Design and Evolution of Object-Oriented Languages 
Mark Hills and Grigore Rosu
OOPSLA'07 Companion, ACM Press, pp 827-828. 2007
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
Technical Report Bericht-Nr. 2007-7, pp. 23-26, July 2007
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
WRLA'06, ENTCS 176(4), pp. 215-231. 2007
PDF, Experiments, ENTCS, WRLA'06, BIB
K: a Rewrite-based Framework for Modular Language Design, Semantics, Analysis and Implementation 
Grigore Rosu
Technical report UIUCDCS-R-2006-2802, December 2006
PDF, TR@UIUC, BIB
Rewriting Logic Semantics: From Language Specifications to Formal Analysis Tools 
Jose Meseguer and Grigore Rosu
IJCAR'04, LNCS 3097, pp 1-44. 2004
PDF, Maude-code, LNCS, IJCAR'04, BIB
Formal Analysis of Java Programs in JavaFAN 
Azadeh Farzan, Feng Chen, Jose Meseguer and Grigore Rosu
CAV'04, LNCS 3114, pp 501 - 505. 2004.
PDF, LNCS, CAV'04, DBLP, BIB
CS322 - Programming Language Design: Lecture Notes 
Grigore Rosu
Technical Report UIUCDCS-R-2003-2897, December 2003
PDF, TR @ UIUC, BIB

Personal tools
Namespaces

Variants
Actions
Navigation