K Publications

From K Framework
Revision as of 01:02, 12 January 2017 by Dpark (Talk | contribs)

(diff) ← Older revision | Latest revision (diff) | Newer revision → (diff)
Jump to: navigation, search

This page provides all K-related publications by its designers and developers.

Select Publications

We recommend citing this paper when you refer to K in your work, in addition to providing its URL (http://kframework.org) in the main text:

  • The first major publication about 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

Here are the most relevant publications to learn about K and what you can do with it:

  • An overview of K and a dynamic and a static K semantics of an imperative language.
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

  • A brief introduction to the current K tool:
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

  • A non-trivial application of K, the most complete formal definition of C to date:
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

  • A non-trivial application of K, the most complete formal definition of Java to date:
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 non-trivial application of K, the most complete formal definition of JavaScript to date:
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


All Publications

Here are all publications about K, in reverse chronological order.

Semantics-Based Program Verifiers for All Languages 
Andrei Stefanescu and Daejun Park and Shijiao Yuwen and Yilong Li and Grigore Rosu
OOPSLA'16, ACM, pp 74-91. 2016
PDF, Slides(PDF), Matching Logic, DOI, OOPSLA'16, BIB
RV-Match: Practical Semantics-Based Program Analysis 
Dwight Guth and Chris Hathhorn and Manasvi Saxena and Grigore Rosu
CAV'16, LNCS 9779, pp 447-453. 2016
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
J.FAOC, Volume 28(3), pp 469-497. 2016
PDF, Matching Logic, DOI, J.FAOC, BIB
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
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
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
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
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
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
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
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
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

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
A Formal Semantics of C with Applications 
Chucky Ellison
PhD Thesis, University of Illinois, July 2012
PDF, Slides, Project, 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
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
A K-Based Formal Framework for Domain-Specific Modelling Languages 
Vlad Rusu and Dorel Lucanu
FoVeOOS'11, to appear
PDF, FoVeOOS'11, BIB
Context Transformers in the K Framework 
Andrei Arusoaie and Traian Florin Serbanuta
K'11. 2011. To appear
PDF, Slides (PDF), K'11, BIB
K Semantics for OCL — a Proposal for a Formal Definition for OCL 
Vlad Rusu and Dorel Lucanu
K'11. 2011. To appear
PDF, Slides (PDF), K'11, 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
Path Directed Symbolic Execution in the K Framework 
Irina Asavoae, Mihail Asavoae and Dorel Lucanu
SYNACS'10, pp 133-141. 2010
PDF, SYNACS'10, BIB
Collecting Semantics under Predicate Abstraction in the K Framework 
Irina Asavoae and Mihail Asavoae
WRLA'10, LNCS 6381, pp 123-139, 2010
DOI, 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
P systems with control nuclei: The concept 
Camelia Chira, Traian Florin Serbanuta and Gheorghe Stefanescu
J.LAP, Volume 79(6), pp 326-333. 2010
PDF, J.LAP, 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