FSL Publications

From FSL

Jump to: navigation, search

Here are all the papers published by the FSL group. Older publications by Grigore Rosu (before joining UIUC) can be found on his previous publications page.


[edit] 2009

Efficient Formalism-Independent Monitoring of Parametric Properties
Image:blank.gifFeng Chen, Patrick Meredith, Dongyun Jin and Grigore Rosu
Image:blank.gifImage:New.gif ASE'09, to appear
Image:blank.gifPDF, ASE'09, BIB
Circular Coinduction with Special Contexts
Image:blank.gifDorel Lucanu and Grigore Rosu
Image:blank.gifImage:New.gif ICFEM'09, to appear in LNCS. 2009
Image:blank.gifPDF, ICFEM'09, BIB
Handling Mixed-Criticality in SoC-based Real-Time Embedded Systems
Image:blank.gifRodolfo Pellizzoni, Patrick Meredith, Min-Young Nam, Mu Sun, Marco Caccamo and Lui Sha
Image:blank.gifEmsoft'09, to appear
Image:blank.gifPDF, Emsoft'09, BIB
Runtime Verification of C Memory Safety
Image:blank.gifGrigore Rosu, Wolfram Schulte and Traian Florin Serbanuta
Image:blank.gifRV'09, LNCS 5779, pp 132-151. 2009
Image:blank.gifPDF, RV slides, RV'09, LNCS, BIB
Circular Coinduction: A Proof Theoretical Foundation
Image:blank.gifGrigore Rosu and Dorel Lucanu
Image:blank.gifCALCO'09, LNCS 5728, pp 127-144. 2009
Image:blank.gifSlides (PDF), LNCS, CALCO'09, DBLP, BIB
From Rewriting Logic Executable Semantics to Matching Logic Program Verification
Image:blank.gifGrigore Rosu, Chucky Ellison and Wolfram Schulte
Image:blank.gifTechnical Report http://hdl.handle.net/2142/13159, July 2009
Image:blank.gifPDF, TR@UIUC, BIB
Matching Logic --- Extended Report
Image:blank.gifGrigore Rosu and Wolfram Schulte
Image:blank.gifTechnical Report UIUCDCS-R-2009-3026, January 2009
Image:blank.gifTR@UIUC, BIB
A Semantic Approach to Interpolation
Image:blank.gifAndrei Popescu, Traian Florin Serbanuta and Grigore Rosu
Image:blank.gifJ. of TCS, Volume 410(12-13), pp 1109-1128. 2009
Image:blank.gifPDF, DOI, BIB
Monitoring Oriented Programming - A Project Overview
Image:blank.gifFeng Chen, Dongyun Jin, Patrick Meredith, and Grigore Rosu
Image:blank.gifICICIS'09, invited paper/talk
Image:blank.gifPDF, ICICIS'09, BIB
A Rewriting Logic Approach to Operational Semantics
Image:blank.gifTraian Florin Serbanuta, Grigore Rosu and Jose Meseguer
Image:blank.gifInformation and Computation, Volume 207(2), pp 305-340. 2009
Image:blank.gifPDF, Experiments, DOI, BIB
Parametric Trace Slicing and Monitoring
Image:blank.gifFeng Chen and Grigore Rosu
Image:blank.gifTACAS'09, LNCS 5505, pp 246-261. 2009.
Image:blank.gifPDF, Slides (PPT), LNCS, TACAS'09, DBLP, BIB
Dependent advice: A general approach to optimizing history-based Aspects
Image:blank.gifEric Bodden, Feng Chen and Grigore Rosu
Image:blank.gifAOSD'09, ACM, pp 3--14. 2009.
Image:blank.gifPDF, TR@ABC, AOSD, BIB

[edit] 2008

Towards a Module System for K
Image:blank.gifMark Hills and Grigore Rosu
Image:blank.gifWADT'08, LNCS, to appear. 2008
Image:blank.gifPDF, WADT'08, BIB
Maximal Causal Models for Multithreaded Systems
Image:blank.gifTraian Florin Serbanuta, Feng Chen and Grigore Rosu
Image:blank.gifImage:New.gif Technical report UIUCDCS-R-2008-3017, December 2008
Image:blank.gifPDF, TR@UIUC, BIB
Hardware Runtime Monitoring for Dependable COTS-based Real-Time Embedded Systems
Image:blank.gifRodolfo Pellizzoni, Patrick Meredith, Marco Caccamo and Grigore Rosu
Image:blank.gifRTSS'08, IEEE, pp. 481-491. 2008
Image:blank.gifPDF, Experiments, RTSS'08 slides, RTSS'08, BIB
Defining and Executing P-systems with Structured Data in K
Image:blank.gifTraian Florin Serbanuta, Gheorghe Stefanescu and Grigore Rosu
Image:blank.gifWMC'08, LNCS 5391, pp 374-393. 2009
Image:blank.gifPDF, Experiments, WMC'08 Slides, WMC'08, DOI, BIB
A Rewriting Logic Approach to Type Inference
Image:blank.gifChucky Ellison, Traian Florin Serbanuta and Grigore Rosu
Image:blank.gifWADT'08 Abstract
Image:blank.gifPDF, WADT'08 Slides PDF, BIB
Efficient Monitoring of Parametric Context-Free Patterns
Image:blank.gifPatrick Meredith, Dongyun Jin, Feng Chen and Grigore Rosu
Image:blank.gifASE'08, IEEE/ACM, pp 148-157. 2008 ACM Sigsoft Distinguished Paper
Image:blank.gifPDF, Experiments, ASE'08 slides(KEY), ASE'08 slides(MOV), ASE'08 slides(PPT), IEEE/ACM ASE'08, BIB
Mining Parametric State-Based Specifications from Executions
Image:blank.gifFeng Chen and Grigore Rosu
Image:blank.gifTechnical report UIUCDCS-R-2008-3000, September 2008
Image:blank.gifPDF, BIB
Parametric Trace Slicing and Monitoring
Image:blank.gifGrigore Rosu and Feng Chen
Image:blank.gifImage:New.gif Technical report UIUCDCS-R-2008-2977, July 2008
Image:blank.gifPDF, TR@UIUC, BIB
A Rewriting Logic Approach to Static Checking of Units of Measurement in C
Image:blank.gifMark Hills, Feng Chen and Grigore Rosu
Image:blank.gifImage:New.gif RULE'08, ENTCS, to appear, 2008
Image:blank.gifPDF, RULE'08 slides, RULE'08, BIB
Efficient Monitoring of Parametric Context-Free Patterns
Image:blank.gifPatrick Meredith, Dongyun Jin, Feng Chen and Grigore Rosu
Image:blank.gifTechnical report UIUCDCS-R-2008-2954, April 2008
Image:blank.gifPDF, TR@UIUC, BIB
Monitoring IVHM Systems using a Monitor-Oriented Programming Framework
Image:blank.gifSudipto Ghoshal, Solaiappan Manimaran, Grigore Rosu, Traian Florin Serbanuta, and Gheorghe Stefanescu
Image:blank.gifLFM 2008
Image:blank.gifPDF, LFM'08 Slides, LFM'08, BIB
jPredictor: A Predictive Runtime Analysis Tool for Java
Image:blank.gifFeng Chen and Traian Florin Serbanuta and Grigore Rosu
Image:blank.gifICSE'08, ACM, pp. 221-230. 2008
Image:blank.gifPDF, ICSE'08 slides, DOI, ICSE'08, BIB
A Rewriting Logic Approach to Defining Type Systems
Image:blank.gifChucky Ellison
Image:blank.gifMaster's Thesis
Image:blank.gifPDF, BIB
A Rewriting Logic Approach to Type Inference
Image:blank.gifChucky Ellison, Traian Florin Serbanuta and Grigore Rosu
Image:blank.gifTechnical report UIUCDCS-R-2008-2934, March 2008
Image:blank.gifPDF, TR@UIUC, BIB
Synthesizing Monitors for Safety Properties -- This Time With Calls and Returns --
Image:blank.gifGrigore Rosu, Feng Chen and Thomas Ball
Image:blank.gifRV'08, LNCS 5289, pp 51-68, 2008
Image:blank.gifPDF, RV'08, BIB
Pluggable Policies for C
Image:blank.gifMark Hills, Feng Chen and Grigore Rosu
Image:blank.gifTechnical Report UIUCDCS-R-2008-2931, January 2008
Image:blank.gifPDF, TR@UIUC, BIB
Memory Representations in Rewriting Logic Semantics Definitions
Image:blank.gifMark Hills
Image:blank.gifImage:New.gif WRLA'08, ENTCS, to appear, 2008
Image:blank.gifPDF, WRLA'08 slides, WRLA'08, BIB


[edit] 2007

K: A Rewriting-Based Framework for Computations -- Preliminary version
Image:blank.gifGrigore Rosu
Image:blank.gifTechnical report UIUCDCS-R-2007-2926 and UILU-ENG-2007-1827, December 2007
Image:blank.gifPDF, ZIP, TR@UIUC, BIB
Synthesizing Monitors for Safety Properties -- This Time With Calls and Returns --
Image:blank.gifGrigore Rosu,Feng Chen and Thomas Ball
Image:blank.gifImage:New.gif Technical report UIUCDCS-R-2007-2908, October 2007
Image:blank.gifPDF, BIB
A K Definition of Scheme
Image:blank.gifPatrick Meredith, Mark Hills and Grigore Rosu
Image:blank.gifTechnical Report UIUCDCS-R-2007-2907, October 2007
Image:blank.gifPDF, TR@UIUC, BIB
Effective Predictive Runtime Analysis Using Sliced Causality and Atomicity
Image:blank.gifFeng Chen, Traian Florin Serbanuta and Grigore Rosu
Image:blank.gifTechnical report UIUCDCS-R-2007-2905, October 2007
Image:blank.gifPDF, TR@UIUC, BIB
An Executable Rewriting Logic Semantics of K-Scheme
Image:blank.gifPatrick Meredith, Mark Hills and Grigore Rosu
Image:blank.gif8th Workshop on Scheme and Functional Programming, Technical Report DIUL-RT-0701, pp. 91-103, September 2007
Image:blank.gifPDF, SCHEME'07, BIB
A Rewriting Approach to the Design and Evolution of Object-Oriented Languages
Image:blank.gifMark Hills and Grigore Rosu
Image:blank.gifOOPSLA'07 Companion, ACM Press, pp 827-828. 2007
Image:blank.gifPDF, OOPSLA'07 poster, ACM, OOPSLA'07, BIB
A Rewriting Approach to the Design and Evolution of Object-Oriented Languages
Image:blank.gifMark Hills and Grigore Rosu
Image:blank.gifTechnical Report Bericht-Nr. 2007-7, pp. 23-26, July 2007
Image:blank.gifPDF, ECOOP'07 Doctoral Symposium slides, ECOOP'07 Doctoral Symposium, BIB
MOP: An Efficient and Generic Runtime Verification Framework
Image:blank.gifFeng Chen and Grigore Rosu
Image:blank.gifOOPSLA'07, ACM press, pp 569-588. 2007
Image:blank.gifPDF, OOPSLA'07 slides, ACM, OOPSLA'07, DBLP, TR@UIUC, BIB
A Rewriting Logic Approach to Operational Semantics -- Extended Abstract
Image:blank.gifTraian Florin Serbanuta, Grigore Rosu and Jose Meseguer
Image:blank.gifSOS'07, ENTCS 192(1), pp 125-141. 2007
Image:blank.gifPDF, SOS'07 Slides, ENTCS, SOS'07, BIB
CIRC: A Circular Coinductive Prover
Image:blank.gifDorel Lucanu and Grigore Rosu
Image:blank.gifCALCO'07, LNCS 4624, pp 372-378. 2007
Image:blank.gifPDF, CIRC webpage, CALCO'07, BIB
Parametric and Sliced Causality
Image:blank.gifFeng Chen and Grigore Rosu
Image:blank.gifCAV'07, LNCS 4590, pp 240 - 253, 2007
Image:blank.gifPDF, CAV'07 slides, CAV'07, TR@UIUC, BIB
KOOL: An Application of Rewriting Logic to Language Prototyping and Analysis
Image:blank.gifMark Hills and Grigore Rosu
Image:blank.gifRTA'07, LNCS 4533, pp 246-256. 2007
Image:blank.gifPDF, RTA'07 slides, LNCS, RTA'07, BIB
On Formal Analysis of OO Languages using Rewriting Logic: Designing for Performance
Image:blank.gifMark Hills and Grigore Rosu
Image:blank.gifFMOODS'07, LNCS 4468, pp 107-121. 2007
Image:blank.gifPDF, FMOODS'07 slides, LNCS, FMOODS'07, BIB
On Safety Properties and Their Monitoring
Image:blank.gifGrigore Rosu
Image:blank.gifImage:New.gif Technical report UIUCDCS-R-2007-2850, February 2007
Image:blank.gifPDF, ZIP, TR@UIUC, BIB
An Effective Algorithm for the Membership Problem for Extended Regular Expressions
Image:blank.gifGrigore Rosu
Image:blank.gifFOSSACS'07, LNCS 4423, pp 332-345, 2007
Image:blank.gifPDF, FOSSACS'07, BIB
The Rewriting Logic Semantics Project
Image:blank.gifJose Meseguer and Grigore Rosu
Image:blank.gifImage:New.gif J. of TCS, Volume 373(3), pp 213-237. 2007
Image:blank.gifPDF, J.TCS, BIB


[edit] 2006

A Rewrite Framework for Language Definitions and for Generation of Efficient Interpreters
Image:blank.gifMark Hills, Traian Florin Serbanuta and Grigore Rosu
Image:blank.gifWRLA'06, ENTCS 176(4), pp. 215-231. 2007
Image:blank.gifPDF, Experiments, ENTCS, WRLA'06, BIB
K: a Rewrite-based Framework for Modular Language Design, Semantics, Analysis and Implementation
Image:blank.gifGrigore Rosu
Image:blank.gifTechnical report UIUCDCS-R-2006-2802, December 2006
Image:blank.gifPDF, TR@UIUC, BIB
A Rewriting Based Approach to OO Language Prototyping and Design
Image:blank.gifMark Hills and Grigore Rosu
Image:blank.gifTechnical Report UIUCDCS-R-2006-2786, October 2006
Image:blank.gifPDF, TR@UIUC, BIB
KOOL: A K-based Object-Oriented Language
Image:blank.gifMark Hills and Grigore Rosu
Image:blank.gifTechnical Report UIUCDCS-R-2006-2779, October 2006
Image:blank.gifPDF, TR@UIUC, BIB
MOP: Reliable Software Development using Abstract Aspects
Image:blank.gifFeng Chen and Grigore Rosu
Image:blank.gifTechnical report UIUCDCS-R-2006-2776, October 2006
Image:blank.gifPDF, TR@UIUC, BIB
Computationally Equivalent Elimination of Conditions - extended abstract
Image:blank.gifTraian Florin Serbanuta and Grigore Rosu
Image:blank.gifRTA'06, LNCS 4098, pp 19-34. 2006
Image:blank.gifPDF, Experiments, RTA'06 Slides, LNCS, RTA'06, DBLP, BIB
GFOL: a Term-Generic Logic for Defining Lambda-Calculi
Image:blank.gifAndrei Popescu and Grigore Rosu
Image:blank.gifImage:New.gif Technical Report UIUCDCS-R-2006-2756, July 2006
Image:blank.gifPDF, TR@UIUC, BIB
Discovering Likely Method Specifications
Image:blank.gifNikolai Tillmann and Feng Chen and Wolfram Schulte
Image:blank.gifICFEM'06, to appear in LNCS, 2006
Image:blank.gifPDF, ICFEM'06, BIB
Equality of Streams is a Pi_2^0-Complete Problem
Image:blank.gifGrigore Rosu
Image:blank.gifICFP'06, ACM, 2006
Image:blank.gifPDF, ICFP'06 Slides, ACM, ICFP'06, BIB
Complete Categorical Deduction for Satisfaction as Injectivity
Image:blank.gifGrigore Rosu
Image:blank.gifFestschrift in Honor of Joseph Goguen, LNCS 4060, pp 157-172. 2006.
Image:blank.gifPDF, Goguen's Festschrift slides, LNCS, Goguen's Festschrift, Goguen's Webpage, BIB
Allen Linear (Interval) Temporal Logic -Translation to LTL and Monitor Synthesis-
Image:blank.gifGrigore Rosu and Saddek Bensalem
Image:blank.gifCAV'06, LNCS 4144, pp 263-277, 2006
Image:blank.gifPDF, CAV'06, CAV'06 Slides, BIB
Parametric and Termination-Sensitive Control Dependence - Extended Abstract
Image:blank.gifFeng Chen and Grigore Rosu
Image:blank.gifSAS'06, LNCS 4134, pp 387-404. 2006.
Image:blank.gifPDF, LNCS, SAS'06, BIB
Parametric and Termination-Sensitive Control Dependence
Image:blank.gifFeng Chen and Grigore Rosu
Image:blank.gifTechnical report UIUCDCS-R-2006-2712, April 2006
Image:blank.gifPDF, TR@UIUC, BIB
A Rewrite Logic Approach to Semantic Definition, Design and Analysis of Object-Oriented Languages
Image:blank.gifFeng Chen, Mark Hills and Grigore Rosu
Image:blank.gifTechnical Report UIUCDCS-R-2006-2702, March 2006
Image:blank.gifPDF, TR@UIUC, BIB
Predicting Concurrency Errors at Runtime using Sliced Causality
Image:blank.gifFeng Chen and Grigore Rosu
Image:blank.gifTechnical report UIUCDCS-R-2006-2965, 2006.
Image:blank.gifPDF, TR@UIUC, BIB
A Semantic Approach to Interpolation
Image:blank.gifAndrei Popescu, Traian Florin Serbanuta and Grigore Rosu
Image:blank.gifFOSSACS'06, LNCS 3921, pp 307-321. 2006
Image:blank.gifPDF, FOSSACS'06 slides, LNCS, FOSSACS '06, DBLP, BIB
Static Analysis to Enforce Safe Value Flow in Embedded Control Systems
Image:blank.gifSumant Kowshik, Grigore Rosu and Lui Sha
Image:blank.gifDSN'06, IEEE, pp 23-34. 2006.
Image:blank.gifPDF, DSN'06 Slides, IEEE, DSN'06, BIB


[edit] 2005

Efficient Monitoring of Omega-Languages
Image:blank.gifMarcelo d'Amorim and Grigore Rosu
Image:blank.gifCAV'05, LNCS 3576, pp 364 - 378. 2005.
Image:blank.gifPDF, LNCS, CAV'05, DBLP, BIB
Behavioral Extensions of Institutions
Image:blank.gifAndrei Popescu and Grigore Rosu
Image:blank.gifCALCO'05, LNCS 3629, pp. 331-347. 2005
Image:blank.gifPDF, CALCO'05 Slides, LNCS , CALCO '05, DBLP, BIB
Checking and Correcting Behaviors of Java Programs at Runtime with Java-MOP
Image:blank.gifFeng Chen, Marcelo d'Amorim and Grigore Rosu
Image:blank.gifRV'05, ENTCS 144, issue 4, pp 3-20. 2005.
Image:blank.gifPDF, ENTCS, RV'05, DBLP, BIB
Predicting Concurrency Errors at Runtime using Sliced Causality
Image:blank.gifFeng Chen and Grigore Rosu
Image:blank.gifTechnical report UIUCDCS-R-2005-2660, 2005.
Image:blank.gifPDF, TR@UIUC, BIB
Java-MOP: A Monitoring Oriented Programming Environment for Java
Image:blank.gifFeng Chen and Grigore Rosu
Image:blank.gifTACAS'05, LNCS 3440, pp 546-550. 2005.
Image:blank.gifPDF, LNCS, TACAS'05, DBLP, BIB
Automatic and Precise Dimensional Analysis
Image:blank.gifMarcelo d'Amorim, Mark Hills, Feng Chen and Grigore Rosu
Image:blank.gifTechnical Report UIUCDCS-R-2005-2668, December 2005
Image:blank.gifPDF, Sources, TR@UIUC, BIB
K: a Rewrite-based Framework for Modular Language Design, Semantics, Analysis and Implementation
Image:blank.gifGrigore Rosu
Image:blank.gifTechnical Report UIUCDCS-R-2005-2672, December 2005
Image:blank.gifPDF, Experiments, BIB
An Executable Semantic Definition of the Beta Language using Rewriting Logic
Image:blank.gifMark Hills, T. Baris Aktemur and Grigore Rosu
Image:blank.gifTechnical Report UIUCDCS-R-2005-2650, November 2005
Image:blank.gifPDF, TR@UIUC, BIB
Rewriting-based Techniques for Runtime Verification
Image:blank.gifGrigore Rosu and Klaus Havelund
Image:blank.gifJ. of ASE, Volume 12(2), pp 151-197. 2005
Image:blank.gifPDF, J.ASE, DBLP, BIB
The Rewriting Logic Semantics Project
Image:blank.gifJose Meseguer and Grigore Rosu
Image:blank.gifSOS'05, ENTCS 156, pp. 27-56. 2006
Image:blank.gifPDF, SOS'05, BIB
An Effective Algorithm for the Membership Problem for Extended Regular Expressions
Image:blank.gifGrigore Rosu
Image:blank.gifTechnical Report UIUCDCS-R-2005-2694, August 2005
Image:blank.gifPDF, Technical Report @ UIUC, BIB


[edit] 2004

Formal Analysis of Java Programs in JavaFAN
Image:blank.gifAzadeh Farzan, Feng Chen, Jose Meseguer and Grigore Rosu
Image:blank.gifCAV'04, LNCS 3114, pp 501 - 505. 2004.
Image:blank.gifPDF, LNCS, CAV'04, DBLP, BIB
Monitoring-Oriented Programming: A Tool-Supported Methodology for Higher Quality Object-Oriented Software
Image:blank.gifFeng Chen, Marcelo d'Amorim and Grigore Rosu
Image:blank.gifTechnical Report UIUCDCS-R-2004-2420, 2004.
Image:blank.gifPDF, TR@UIUC, BIB
A Formal Monitoring-based Framework for Software Development and Analysis
Image:blank.gifFeng Chen and Marcelo d'Amorim and Grigore Rosu
Image:blank.gifICFEM'04, LNCS 3308, pp 357 - 373. 2004.
Image:blank.gifPDF, LNCS, ICFEM'04, DBLP, BIB
From Conditional to Unconditional Rewriting
Image:blank.gifGrigore Rosu
Image:blank.gifWADT'04, LNCS 3423, pp 218-233. 2004
Image:blank.gifPDF, LNCS, WADT'04, Experiments, PDF - Original submission, WADT'04 slides, BIB
From Conditional to Unconditional Rewriting
Image:blank.gifGrigore Rosu
Image:blank.gifTechnical Report UIUCDCS-R-2004-2471, August 2004
Image:blank.gifPDF, Technical reports' page, Experiments, BIB
Behavioral Abstraction is Hiding Information
Image:blank.gifGrigore Rosu
Image:blank.gifJ. of TCS, Volume 327(1-2), pp 197-221. 2004
Image:blank.gifPDF, J.TCS, BIB


[edit] 2003

Certifying Measurement Unit Safety Policy
Image:blank.gifGrigore Rosu and Feng Chen
Image:blank.gifASE'03, IEEE, pp. 304 - 309. 2003.
Image:blank.gifPDF, IEEE, ASE'03, BIB
Rule-Based Analysis of Dimensional Safety
Image:blank.gifFeng Chen and Grigore Rosu and Ram Prasad Venkatesan
Image:blank.gifRTA'03, LNCS 2706, pp197 - 207. 2003.
Image:blank.gifPDF, LNCS, RTA'03, DBLP, BIB
Towards Monitoring-Oriented Programming: A Paradigm Combining Specification and Implementation
Image:blank.gifFeng Chen and Grigore Rosu
Image:blank.gifRV'03, ENTCS 89, issue 2, pp 108 - 127. 2003.
Image:blank.gifPDF, ENTCS, RV'03, DBLP, BIB
CS322 - Programming Language Design: Lecture Notes
Image:blank.gifGrigore Rosu
Image:blank.gifTechnical Report UIUCDCS-R-2003-2897, December 2003
Image:blank.gifPDF, TR @ UIUC, BIB
Inductive Behavioral Proofs by Unhiding
Image:blank.gifGrigore Rosu
Image:blank.gifCMCS'03, ENTCS 82(1). 2003
Image:blank.gifPDF, ENTCS, CMCS'03, Experiments, DBLP, BIB

Retrieved from "http://fsl.cs.uiuc.edu/index.php/FSL_Publications"
Views
Personal tools