Rewriting Logic Semantics

From FSL
Jump to: navigation, search

Rewriting logic can be used to create executable definitions of programming languages, yielding interpreters for the defined languages which run programs directly in the language semantics. This also yields definitions of languages that can be used for formal reasoning about language properties. Examples include model checking, state-space exploration for programs with potentially unbounded state spaces, theorem proving, partial correctness via Hoare logics, and type safety/type checking.

Contents

Definitions of Existing Languages

We have defined several existing languages using rewriting logic. These definitions can be used to both run programs in the defined language and reason about the language, and have been used in a number of contexts.

  • Lambda Calculus, a commonly-used language calculus which has served as a model for many functional languages
  • Beta, a statically-typed object-oriented programming language derived from Simula 67, where the unifying concept of pattern has replaced classes and methods
  • Java, a statically-typed, class-based object-oriented programming language
  • Prolog, a logic programming language (only partially defined)
  • Scheme, a very faithful semantics of Scheme, a functional language with strong reflection and meta-programming capabilities.

Definitions of Sample Languages

We have also defined a number of research languages using rewriting logic. These have value both as examples of specific paradigms of languages (functional, imperative, object-oriented) and as basis languages which we can use in our research.

  • SILF, a Simple Imperative Language with Functions, used for illustrating our framework
  • CSILF, a Concurrent version of SILF, used to illustrate the addition of simple concurrency features and verification of concurrent programs
  • KOOL, a dynamically typed object-oriented language

Annotated Bibliography

This bibliography provides a set of related readings for those interested in rewriting logic semantics and our approach to defining executable semantics for languages. Click Rewriting Logic Semantics Readings for more information.

Publications

Self-organising assembly systems formally specified in Maude 
Regina Frei, Traian Florin Serbanuta and Giovanna Di Marzo Serugendo
J.AIHC, to appear. 2012
PDF, 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
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, SVN, 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
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, SVN, 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
Automating Coinduction with Case Analysis 
Eugen-Ioan Goriac, Dorel Lucanu and Grigore Rosu
ICFEM'10, LNCS 6447, pp 220-236. 2010
PDF, LNCS, ICFEM'10, CIRC, 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
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
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
Towards a Module System for K 
Mark Hills and Grigore Rosu
WADT'08, LNCS 5486, pp 187-205. 2009
PDF, LNCS, WADT'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
Memory Representations in Rewriting Logic Semantics Definitions 
Mark Hills
WRLA'08, ENTCS, to appear, 2008
PDF, WRLA'08 slides, WRLA'08, 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
Technical Report Bericht-Nr. 2007-7, pp. 23-26, July 2007
PDF, ECOOP'07 Doctoral Symposium slides, ECOOP'07 Doctoral Symposium, BIB
A Rewriting Logic Approach to Operational Semantics -- Extended Abstract 
Traian Florin Serbanuta, Grigore Rosu and Jose Meseguer
SOS'07, ENTCS 192(1), pp 125-141. 2007
PDF, Slides (PPT), ENTCS, SOS'07, BIB
KOOL: An Application of Rewriting Logic to Language Prototyping and Analysis 
Mark Hills and Grigore Rosu
RTA'07, LNCS 4533, pp 246-256. 2007
PDF, RTA'07 slides, LNCS, RTA'07, BIB
On Formal Analysis of OO Languages using Rewriting Logic: Designing for Performance 
Mark Hills and Grigore Rosu
FMOODS'07, LNCS 4468, pp 107-121. 2007
PDF, FMOODS'07 slides, LNCS, FMOODS'07, BIB
The Rewriting Logic Semantics Project 
Jose Meseguer and Grigore Rosu
J. of TCS, Volume 373(3), pp 213-237. 2007
PDF, J.TCS, 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
A Rewriting Based Approach to OO Language Prototyping and Design 
Mark Hills and Grigore Rosu
Technical Report UIUCDCS-R-2006-2786, October 2006
PDF, TR@UIUC, BIB
KOOL: A K-based Object-Oriented Language 
Mark Hills and Grigore Rosu
Technical Report UIUCDCS-R-2006-2779, October 2006
PDF, TR@UIUC, BIB
Haskell-RL: An Equational Specification of Haskell in Maude 
Andrew Bennett
MS CS Thesis Submission
PDF, semantics
A Rewrite Logic Approach to Semantic Definition, Design and Analysis of Object-Oriented Languages 
Feng Chen, Mark Hills and Grigore Rosu
Technical Report UIUCDCS-R-2006-2702, March 2006
PDF, TR@UIUC, BIB
K: a Rewrite-based Framework for Modular Language Design, Semantics, Analysis and Implementation 
Grigore Rosu
Technical Report UIUCDCS-R-2005-2672, December 2005
PDF, Experiments, BIB
An Executable Semantic Definition of the Beta Language using Rewriting Logic 
Mark Hills, T. Baris Aktemur and Grigore Rosu
Technical Report UIUCDCS-R-2005-2650, November 2005
PDF, TR@UIUC, BIB
The Rewriting Logic Semantics Project 
Jose Meseguer and Grigore Rosu
SOS'05, ENTCS 156, pp. 27-56. 2006
PDF, SOS'05, 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
Hidden Logic 
Grigore Rosu
PhD Thesis, University of California at San Diego
PDF, Thesis@UCSD, BIB

Other Presentations

Current progress, as of April 2006, presented at 25px-Pdf_icon.png MSPLS Spring 2006 Info_circle.png.

Personal tools
Namespaces

Variants
Actions
Navigation