K Publications

From K Framework

Jump to: navigation, search

Defining the Undefinedness of C 
Chucky Ellison and Grigore Rosu
Technical Report http://hdl.handle.net/2142/30780, April 2012
PDF, TR@UIUC, BIB
The K Framework Distilled 
Dorel Lucanu, Grigore Rosu and Traian Florin Serbanuta
WRLA'12 invited paper, LNCS, to appear
Slides (PDF), WRLA'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, to appear
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
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
An Executable Formal Semantics of C with Applications 
Chucky Ellison and Grigore Rosu
Technical Report http://hdl.handle.net/2142/25816, July 2011
PDF, Coverage Results, Project, TR@UIUC, SVN, 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 Semantics of C with Applications 
Chucky Ellison and Grigore Rosu
Technical Report http://hdl.handle.net/2142/17414, November 2010
PDF, Correctness Results, Coverage Results, Project, TR@UIUC, 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
KRAM—Extended Report 
Traian Florin Serbanuta and Grigore Rosu
Technical Report http://hdl.handle.net/2142/17337, September 2010
PDF, TR@UIUC, 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