FSL Publications

From FSL
Revision as of 23:59, 24 February 2016 by Yzhng173 (Talk | contribs)

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.

2016

Semantics-Based Program Verifiers for All Languages
Blank.gifAndrei Stefanescu and Daejun Park and Shijiao Yuwen and Yilong Li and Grigore Rosu
Blank.gifOOPSLA'16, ACM, pp 74-91. 2016
Blank.gifPDF, Slides(PDF), Matching Logic, DOI, OOPSLA'16, BIB
Finite-Trace Linear Temporal Logic: Coinductive Completeness
Blank.gifGrigore Rosu
Blank.gifRV'16, LNCS 10012, pp 333-350. 2016
Blank.gifPDF, Slides(PPTX), Matching Logic, DOI, RV'16, BIB
Runtime Verification at Work: A Tutorial
Blank.gifPhilip Daian and Dwight Guth and Chris Hathhorn and Yilong Li and Edgar Pek and Manasvi Saxena and Traian Florin Serbanuta and Grigore Rosu
Blank.gifRV'16, LNCS 10012, pp 46-67. 2016
Blank.gifPDF, Slides(PPTX), RV Products, DOI, RV'16, BIB
How Good are the Specs? A Study of the Bug-Finding Effectiveness of Existing Java API Specifications
Blank.gifOwolabi Legunsen and Wajih Ul Hassan and Xinyue Xu and Grigore Rosu and Darko Marinov
Blank.gifASE 2016, IEEE/ACM, pp 602-613. 2016
Blank.gifPDF, Slides(PDF), JavaMOP, DOI, ASE 2016, BIB
RV-Match: Practical Semantics-Based Program Analysis
Blank.gifDwight Guth and Chris Hathhorn and Manasvi Saxena and Grigore Rosu
Blank.gifCAV'16, LNCS 9779, pp 447-453. 2016
Blank.gifPDF, RV-Match, DOI, CAV'16, BIB
A Language-Independent Proof System for Full Program Equivalence
Blank.gifStefan Ciobaca and Dorel Lucanu and Vlad Rusu and Grigore Rosu
Blank.gifJ.FAOC, Volume 28(3), pp 469-497. 2016
Blank.gifPDF, Matching Logic, DOI, J.FAOC, BIB
RV-ECU: Maximum Assurance In-Vehicle Safety Monitoring
Blank.gifPhilip Daian and Bhargava Manja and Shinichi Shiraishi and Akihito Iwai and Grigore Rosu
Blank.gifSAE'16, SAE International 2016-01-0126, pp 1-13. 2016
Blank.gifPDF, Slides(PPT), RV-ECU, DOI, SAE'16, BIB
Open Problems and Challenges 2016
Blank.gifGrigore Rosu
Blank.gifTechnical Report http://hdl.handle.net/2142/88925, February 2016
Blank.gifPDF, Webpage, DOI, BIB
Language Definitions as Rewrite Theories
Blank.gifVlad Rusu and Dorel Lucanu and Traian Florin Serbanuta and Andrei Arusoaie and Andrei Stefanescu and Grigore Rosu
Blank.gifJ.LAMP, Volume 85(1, Part 1), pp 98-120. 2016
Blank.gifPDF, project, DOI, J.LAMP, BIB
Towards a Kool Future
Blank.gifDorel Lucanu and Traian Florin Serbanuta and Grigore Rosu
Blank.gifBoer's Festschrift, LNCS 9660, pp 325-343. 2016
Blank.gifPDF, K, DOI, Boer's Festschrift, BIB

2015

From Rewriting Logic, to Programming Language Semantics, to Program Verification
Blank.gifGrigore Rosu
Blank.gifMeseguer's Festschrift, LNCS 9200, pp 598-616. 2015
Blank.gifPDF, Slides(PPTX), K, DOI, Meseguer's Festschrift, BIB
RV-Android: Efficient Parametric Android Runtime Verification, a Brief Tutorial
Blank.gifPhilip Daian and Ylies Falcone and Patrick Meredith and Traian Florin Serbanuta and Shinichi Shiraishi and Akihito Iwai and Grigore Rosu
Blank.gifRV'15, Lecture Notes in Computer Science 9333, pp 342-357. 2015
Blank.gifPDF, Slides(PDF), RV-Android, DOI, RV'15, BIB
Matching Logic --- Extended Abstract
Blank.gifGrigore Rosu
Blank.gifRTA'15, Leibniz International Proceedings in Informatics (LIPIcs) 36, pp 5-21. 2015
Blank.gifPDF, Slides(PPTX), Matching Logic, DOI, RTA'15, BIB
Defining the Undefinedness of C
Blank.gifChris Hathhorn and Chucky Ellison and Grigore Rosu
Blank.gifPLDI'15, ACM, pp 336-345. 2015
Blank.gifPDF, C Semantics, DOI, PLDI'15, BIB
KJS: A Complete Formal Semantics of JavaScript
Blank.gifDaejun Park and Andrei Stefanescu and Grigore Rosu
Blank.gifPLDI'15, ACM, pp 346-356. 2015
Blank.gifPDF, Slides(PDF), Semantics, DOI, PLDI'15, BIB
GPredict: Generic Predictive Concurrency Analysis
Blank.gifJeff Huang and Qingzhou Luo and Grigore Rosu
Blank.gifICSE'15, ACM, pp 847-857. 2015
Blank.gifPDF, Slides(PDF), jPredictor, DOI, ICSE'15, BIB
Evolution-Aware Monitoring-Oriented Programming
Blank.gifOwolabi Legunsen and Darko Marinov and Grigore Rosu
Blank.gifICSE NIER'15, ACM, pp 615-618. 2015
Blank.gifPDF, Slides(PDF), JavaMOP, DOI, ICSE NIER'15, BIB
Term-Generic Logic
Blank.gifAndrei Popescu and Grigore Rosu
Blank.gifJournal of Theoretical Computer Science, Volume 577(1), pp 1-24. 2015
Blank.gifPDF, project, DOI, Journal of Theoretical Computer Science, BIB
Program Verification by Coinduction
Blank.gifBrandon Moore and Grigore Rosu
Blank.gifTechnical Report http://hdl.handle.net/2142/73177, February 2015
Blank.gifPDF, Matching Logic, DOI, BIB
K-Java: A Complete Semantics of Java
Blank.gifDenis Bogdanas and Grigore Rosu
Blank.gifPOPL'15, ACM, pp 445-456. 2015
Blank.gifPDF, Slides(PDF), K-Java, DOI, POPL'15, BIB

2014

A Language-Independent Proof System for Mutual Program Equivalence
Blank.gifStefan Ciobaca and Dorel Lucanu and Vlad Rusu and Grigore Rosu
Blank.gifICFEM'14, LNCS 8829, pp 75-90. 2014
Blank.gifPDF, Slides(PDF), Matching Logic, DOI, ICFEM'14, BIB
ROSRV: Runtime Verification for Robots
Blank.gifJeff Huang and Cansu Erdogan and Yi Zhang and Brandon Moore and Qingzhou Luo and Aravind Sundaresan and Grigore Rosu
Blank.gifRV'14, LNCS 8734, pp 247-254. 2014
Blank.gifPDF, Slides(PPTX), Slides(PDF), ROSRV, DOI, RV'14, BIB
RV-Monitor: Efficient Parametric Runtime Verification with Simultaneous Properties
Blank.gifQingzhou Luo and Yi Zhang and Choonghwan Lee and Dongyun Jin and Patrick O'Neil Meredith and Traian Florin Serbanuta and Grigore Rosu
Blank.gifRV'14, LNCS 8734, pp 285-300. 2014
Blank.gifPDF, Slides(PPTX), JavaMOP, DOI, RV'14, BIB
Converting Parallel Code from Low-Level Abstractions to Higher-Level Abstractions
Blank.gifSemih Okur and Cansu Erdogan and Danny Dig
Blank.gifECOOP'14, Springer, pp 515-540. 2014
Blank.gifPDF, Taskifier, DOI, ECOOP'14, BIB
All-Path Reachability Logic
Blank.gifAndrei Stefanescu and Stefan Ciobaca and Radu Mereuta and Brandon Moore and Traian Florin Serbanuta and Grigore Rosu
Blank.gifRTA'14, LNCS 8560, pp 425-440. 2014
Blank.gifPDF, Slides(PPTX), Matching Logic, DOI, RTA'14, BIB
Maximal Sound Predictive Race Detection with Control Flow Abstraction
Blank.gifJeff Huang and Patrick Meredith and Grigore Rosu
Blank.gifPLDI'14, ACM, pp 337-348. 2014
Blank.gifPDF, Slides(PPT), Slides(PDF), jPredictor, DOI, PLDI'14, BIB
On the Complexity of Stream Equality
Blank.gifJoerg Endrullis and Dimitri Hendriks and Rena Bakhshi and Grigore Rosu
Blank.gifJournal of Functional Programming, Volume 24(2-3), pp 166-217. 2014
Blank.gifPDF, CIRC, DOI, Journal of Functional Programming, BIB
Language Definitions as Rewrite Theories
Blank.gifAndrei Arusoaie and Dorel Lucanu and Vlad Rusu and Traian Florin Serbanuta and Andrei Stefanescu and Grigore Rosu
Blank.gifWRLA'14, LNCS 8663, pp 97-112. 2014
Blank.gifPDF, K, DOI, WRLA'14, BIB
Behavioral Rewrite Systems and Behavioral Productivity
Blank.gifGrigore Rosu and Dorel Lucanu
Blank.gifFutatsugi Festschrift 2014, LNCS 8373, pp 296-314. 2014
Blank.gifPDF, Slides(PPTX), CIRC, DOI, Futatsugi Festschrift 2014, BIB
Optimizing SYB is Easy!
Blank.gifMichael D. Adams and Andrew Farmer and Jose Pedro Magalhaes
Blank.gifPEPM'14, ACM, pp 71-82. 2014
Blank.gifPDF, Optimizing SYB, DOI, PEPM'14, BIB
Matching Logic: A Logic for Structural Reasoning
Blank.gifGrigore Rosu
Blank.gifTechnical Report http://hdl.handle.net/2142/47004, Jan 2014
Blank.gifPDF, Matching Logic, DOI, BIB

2013

K Overview and SIMPLE Case Study
Blank.gifGrigore Rosu and Traian Florin Serbanuta
Blank.gifK'11, ENTCS 304, pp 3-56. 2014
Blank.gifPDF, K, DOI, K'11, BIB
Abstract Semantics for K Module Composition
Blank.gifCodruta Girlea and Grigore Rosu
Blank.gifK'11, ENTCS 304, pp 127-149. 2014
Blank.gifPDF, K, DOI, K'11, BIB
The K Primer (version 3.3)
Blank.gifTraian Florin Serbanuta and Andrei Arusoaie and David Lazar and Chucky Ellison and Dorel Lucanu and Grigore Rosu
Blank.gifK'11, ENTCS 304, pp 57-80. 2014
Blank.gifPDF, K, DOI, K'11, BIB
The Rewriting Logic Semantics Project: A Progress Report
Blank.gifJose Meseguer and Grigore Rosu
Blank.gifInformation and Computation, Volume 231(1), pp 38-69. 2013
Blank.gifPDF, K, DOI, Information and Computation, BIB
Specifying Languages and Verifying Programs with K
Blank.gifGrigore Rosu
Blank.gifSYNASC'13, IEEE/CPS, pp 28-31. 2013
Blank.gifPDF, Slides(PPTX), K, DOI, SYNASC'13, BIB
EnforceMOP: A Runtime Property Enforcement System for Multithreaded Programs
Blank.gifQingzhou Luo and Grigore Rosu
Blank.gifISSTA'13, ACM, pp 156-166. 2013
Blank.gifPDF, Slides(PPTX), EnforceMOP, DOI, ISSTA'13, BIB
One-Path Reachability Logic
Blank.gifGrigore Rosu and Andrei Stefanescu and Stefan Ciobaca and Brandon Moore
Blank.gifLICS'13, IEEE, pp 358-367. 2013
Blank.gifPDF, Slides(PPTX), Reachability Logic, LICS'13, BIB
Low-Level Program Verification using Matching Logic Reachability
Blank.gifDwight Guth and Andrei Stefanescu and Grigore Rosu
Blank.gifLOLA'13. 2013
Blank.gifPDF, Slides(PDF), Matching Logic, LOLA'13, BIB
Efficient Parametric Runtime Verification with Deterministic String Rewriting
Blank.gifPatrick Meredith and Grigore Rosu
Blank.gifASE'13, IEEE/ACM, pp 70-80. 2013
Blank.gifPDF, Slides(PPT), Slides(KEY), Slides(PDF), MOP, DOI, ASE'13, BIB

2012

A Truly Concurrent Semantics for the K Framework Based on Graph Transformations
Blank.gifTraian Florin Serbanuta and Grigore Rosu
Blank.gifICGT'12, LNCS 7562, pp 294-310. 2012
Blank.gifPDF, ICGT'12, Slides(PDF), BIB
Maximal Causal Models for Sequentially Consistent Systems
Blank.gifTraian Florin Serbanuta, Feng Chen and Grigore Rosu
Blank.gifRV'12, LNCS. 7687, pp 136-150. 2013
Blank.gifPDF, Slides(PDF), BIB
Checking Reachability using Matching Logic
Blank.gifGrigore Rosu and Andrei Stefanescu
Blank.gifOOPSLA'12, ACM, pp 555-574. 2012
Blank.gifPDF, Slides(pptx), Slides(pdf), Matching Logic, OOPSLA'12, BIB
Efficient, Expressive, and Effective Runtime Verification
Blank.gifPatrick Meredith
Blank.gifPhD Thesis, University of Illinois, August 2012
Blank.gifPDF, Slides(KEY), Slides(PDF), JavaMOP Project, BusMOP Project, RV-Predict Project, BIB
Making Runtime Monitoring of Parametric Properties Practical
Blank.gifDongyun Jin
Blank.gifPhD Thesis, University of Illinois, August 2012
Blank.gifPDF, Slides (PDF), JavaMOP, Sources, BIB
Reachability Logic
Blank.gifGrigore Rosu, Andrei Stefanescu, Stefan Ciobaca and Brandon Moore
Blank.gifTechnical Report http://hdl.handle.net/2142/32952, July 2012
Blank.gifPDF, TR@UIUC
A Formal Semantics of C with Applications
Blank.gifChucky Ellison
Blank.gifPhD Thesis, University of Illinois, July 2012
Blank.gifPDF, Slides, Project, BIB
From Hoare Logic to Matching Logic Reachability
Blank.gifGrigore Rosu and Andrei Stefanescu
Blank.gifFM'12, LNCS 7436, pp 387-402. 2012
Blank.gifPDF, Slides(pptx), Slides(pdf), Matching Logic, FM'12, , BIB
Security-Policy Monitoring and Enforcement with JavaMOP
Blank.gifSoha Hussein, Patrick Meredith and Grigore Rosu
Blank.gifPLAS'12, ACM, pp 3:1-3:11. 2012
Blank.gifPDF, Slides(KEY), Slides(PDF), ACM, PLAS'12, BIB
Executing Formal Semantics with the K Tool
Blank.gifDavid Lazar, Andrei Arusoaie, Traian Florin Serbanuta, Chucky Ellison, Radu Mereuta, Dorel Lucanu and Grigore Rosu
Blank.gifFM'12, LNCS 7436, pp 267-271. 2012
Blank.gifPDF, Slides(PDF), FM'12, DBLP, BIB
Towards a Unified Theory of Operational and Axiomatic Semantics
Blank.gifGrigore Rosu and Andrei Stefanescu
Blank.gifICALP'12, LNCS 7392, pp 351-363. 2012
Blank.gifPDF, Slides(pptx), Slides(pdf), Matching Logic, ICALP'12, BIB
Defining the Undefinedness of C
Blank.gifChucky Ellison and Grigore Rosu
Blank.gifTechnical Report http://hdl.handle.net/2142/30780, April 2012
Blank.gifPDF, TR@UIUC, BIB
Scalable Parametric Runtime Monitoring
Blank.gifDongyun Jin, Patrick Meredith and Grigore Rosu
Blank.gifTechnical Report http://hdl.handle.net/2142/30757, April 2012
Blank.gifPDF, TR@UIUC, BIB
K Framework Distilled
Blank.gifDorel Lucanu, Traian Florin Serbanuta and Grigore Rosu
Blank.gifWRLA'12, LNCS 7571, pp 31-53. 2012 Invited Paper
Blank.gifPDF, Slides (PDF), WRLA'12, LNCS, BIB
JavaMOP: Efficient Parametric Runtime Monitoring Framework
Blank.gifDongyun Jin, Patrick Meredith, Choonghwan Lee and Grigore Rosu
Blank.gifICSE'12, IEEE, pp 1427-1430. 2012
Blank.gifPDF, Demo Movie, TOOL ICSE'12, BIB
Towards Categorizing and Formalizing the JDK API
Blank.gifChoonghwan Lee, Dongyun Jin, Patrick Meredith and Grigore Rosu
Blank.gifTechnical Report http://hdl.handle.net/2142/30006, March 2012
Blank.gifPDF, TR@UIUC, BIB
Test-Case Reduction for C Compiler Bugs
Blank.gifJohn Regehr, Yang Chen, Pascal Cuoq, Eric Eide, Chucky Ellison and Xuejun Yang
Blank.gifPLDI'12, ACM, pp 335-346. 2012
Blank.gifPDF, Slides(PPT), Project, ACM, PLDI'12, DBLP, BIB
Semantics and Algorithms for Parametric Monitoring
Blank.gifGrigore Rosu and Feng Chen
Blank.gifJ.LMCS, Volume 8(1), pp 1-47. 2012
Blank.gifPDF, MOP, J.LMCS, BIB
The K Primer (version 2.5)
Blank.gifTraian Florin Serbanuta, Andrei Arusoaie, David Lazar, Chucky Ellison, Dorel Lucanu and Grigore Rosu
Blank.gifTechnical Report, January 2012
Blank.gifPDF, K 2.5, BIB
Making Maude Definitions more Interactive
Blank.gifAndrei Arusoaie, Traian Florin Serbanuta, Chucky Ellison and Grigore Rosu
Blank.gifWRLA'12, LNCS 7571. 2012
Blank.gifPDF, Slides (PDF), WRLA'12, BIB
Recursive Proofs for Inductive Tree Data-Structures
Blank.gifParthasarathy Madhusudan, Xiaokang Qiu and Andrei Stefanescu
Blank.gifPOPL'12, ACM, pp 123-136, 2012
Blank.gifPDF, Slides(pptx), Slides(pdf), Dryad, ACM, POPL'12, BIB
An Executable Formal Semantics of C with Applications
Blank.gifChucky Ellison and Grigore Rosu
Blank.gifPOPL'12, ACM, pp 533-544. 2012
Blank.gifPDF, Slides(PDF), Project, ACM, POPL'12, DBLP, BIB

2012(NEW)

On Safety Properties and Their Monitoring
Blank.gifGrigore Rosu
Blank.gifSACS, Volume 22(2), pp 327-365. 2012
Blank.gifPDF, MOP, DOI, SACS, BIB
Checking Reachability using Matching Logic
Blank.gifGrigore Rosu and Andrei Stefanescu
Blank.gifOOPSLA'12, ACM, pp 555-574. 2012
Blank.gifPDF, Slides(PPTX), Slides(PDF), Matching Logic, DOI, OOPSLA'12, BIB
A Truly Concurrent Semantics for the K Framework Based on Graph Transformations
Blank.gifTraian Florin Serbanuta and Grigore Rosu
Blank.gifICGT'12, LNCS 7562, pp 294-310. 2012
Blank.gifPDF, Slides(PDF), K, DOI, ICGT'12, BIB
Maximal Causal Models for Sequentially Consistent Systems
Blank.gifTraian Florin Serbanuta and Feng Chen and Grigore Rosu
Blank.gifRV'12, LNCS 7687, pp 136-150. 2012
Blank.gifPDF, Slides(PDF), JPredictor, DOI, RV'12, BIB
From Hoare Logic to Matching Logic Reachability
Blank.gifGrigore Rosu and Andrei Stefanescu
Blank.gifFM'12, LNCS 7436, pp 387-402. 2012
Blank.gifPDF, Slides(PPTX), Slides(PDF), Matching Logic, DOI, FM'12, BIB
Executing Formal Semantics with the K Tool
Blank.gifDavid Lazar and Andrei Arusoaie and Traian Florin Serbanuta and Chucky Ellison and Radu Mereuta and Dorel Lucanu and Grigore Rosu
Blank.gifFM'12, LNCS 7436, pp 267-271. 2012
Blank.gifPDF, Slides(PDF), K, DOI, FM'12, BIB
Making Runtime Monitoring of Parametric Properties Practical
Blank.gifDongyun Jin
Blank.gifPhD Thesis, University of Illinois at Urbana-Champaign. August 2012
Blank.gifPDF, MOP, DOI, BIB
Efficient, Expressive, and Effective Runtime Verification
Blank.gifPatrick O'Neil Meredith
Blank.gifPhD Thesis, University of Illinois at Urbana-Champaign. August 2012
Blank.gifPDF, MOP, DOI, BIB
Reachability Logic
Blank.gifGrigore Rosu and Andrei Stefanescu and Stefan Ciobaca and Brandon Moore
Blank.gifTechnical Report http://hdl.handle.net/2142/32952, Jul 2012
Blank.gifPDF, Reachability Logic, DOI, BIB
Towards a Unified Theory of Operational and Axiomatic Semantics
Blank.gifGrigore Rosu and Andrei Stefanescu
Blank.gifICALP'12, LNCS 7392, pp 351-363. 2012
Blank.gifPDF, Slides(PPTX), Slides(PDF), Matching Logic, DOI, ICALP'12, BIB
A Formal Semantics of C with Applications
Blank.gifChucky Ellison
Blank.gifPhD Thesis, University of Illinois. July 2012
Blank.gifPDF, K, DOI, BIB
Test-Case Reduction for C Compiler Bugs
Blank.gifJohn Regehr and Yang Chen and Pascal Cuoq and Eric Eide and Chucky Ellison and Xuejun Yang
Blank.gifPLDI'12, ACM, pp 335-346. 2012
Blank.gifPDF, Slides(PPTX), C-Reduce, DOI, PLDI'12, BIB
JavaMOP: Efficient Parametric Runtime Monitoring Framework
Blank.gifDongyun Jin and Patrick O'Neil Meredith and Choonghwan Lee and Grigore Rosu
Blank.gifICSE'12, IEEE, pp 1427-1430. 2012
Blank.gifPDF, MOP, DOI, ICSE'12, BIB
Security-Policy Monitoring and Enforcement with JavaMOP
Blank.gifSoha Hussein and Patrick Meredith and Grigore Rosu
Blank.gifPLAS'12, ACM, pp 3:1-3:11. 2012
Blank.gifPDF, MOP, DOI, PLAS'12, BIB
Defining the Undefinedness of C
Blank.gifChucky Ellison and Grigore Rosu
Blank.gifTechnical Report http://hdl.handle.net/2142/30780, April 2012
Blank.gifPDF, K, DOI, BIB
Scalable Parametric Runtime Monitoring
Blank.gifDongyun Jin and Patrick O'Neil Meredith and Grigore Rosu
Blank.gifTechnical Report http://hdl.handle.net/2142/30757, April 2012
Blank.gifPDF, MOP, DOI, BIB
Towards Categorizing and Formalizing the JDK API
Blank.gifChoonghwan Lee and Dongyun Jin and Patrick O'Neil Meredith and Grigore Rosu
Blank.gifTechnical Report http://hdl.handle.net/2142/30006, March 2012
Blank.gifPDF, Java API, DOI, BIB
Making Maude Definitions more Interactive
Blank.gifAndrei Arusoaie and Traian Florin Serbanuta and Chucky Ellison and Grigore Rosu
Blank.gifWRLA'12, LNCS 7571, pp 83-98. 2012
Blank.gifPDF, K, DOI, WRLA'12, BIB
K Framework Distilled
Blank.gifDorel Lucanu and Traian Florin Serbanuta and Grigore Rosu
Blank.gifWRLA'12, LNCS 7571, pp 31-53. 2012
Blank.gifPDF, K, DOI, WRLA'12, BIB
Semantics and Algorithms for Parametric Monitoring
Blank.gifGrigore Rosu and Feng Chen
Blank.gifJ.LMCS, Volume 8(1), pp 1-47. 2012
Blank.gifPDF, MOP, DOI, J.LMCS, BIB
An Executable Formal Semantics of C with Applications
Blank.gifChucky Ellison and Grigore Rosu
Blank.gifPOPL'12, ACM, pp 533-544. 2012
Blank.gifPDF, Slides(PDF), Semantics, DOI, POPL'12, BIB
Recursive Proofs for Inductive Tree Data-Structures
Blank.gifParthasarathy Madhusudan and Xiaokang Qiu and Andrei Stefanescu
Blank.gifPOPL'12, ACM, pp 123-136. 2012
Blank.gifPDF, Dryad, DOI, POPL'12, BIB

2011

Matching Logic Rewriting: Unifying Operational and Axiomatic Semantics in a Practical and Generic Framework
Blank.gifGrigore Rosu and Andrei Stefanescu
Blank.gifTechnical Report http://hdl.handle.net/2142/28357, November 2011
Blank.gifPDF, Matching Logic, TR@UIUC, , BIB
The Rewriting Logic Semantics Project: A Progress Report
Blank.gifJose Meseguer and Grigore Rosu
Blank.gifFCT'11, LNCS 6914, pp 1-37. Invited talk. 2011
Blank.gifPDF, K Tool, FCT'11, BIB
Improved Multithreaded Unit Testing
Blank.gifVilas Jagannath, Milos Gligoric, Dongyun Jin, Qingzhou Luo, Grigore Rosu and Darko Marinov
Blank.gifFSE'11, ACM, pp 223-233. 2011
Blank.gifPDF, FSE'11, BIB
Matching Logic: A New Program Verification Approach (NIER Track)
Blank.gifGrigore Rosu and Andrei Stefanescu
Blank.gifICSE'11, ACM, pp. 868-871. 2011
Blank.gifPDF, Slides(pptx), Slides(pdf), Poster(pptx), Poster(pdf), Matching Logic, ACM, NIER ICSE'11, BIB
Garbage Collection for Monitoring Parametric Properties
Blank.gifDongyun Jin, Patrick Meredith, Dennis Griffith and Grigore Rosu
Blank.gifPLDI'11, ACM, pp 415-424. 2011
Blank.gifPDF, PLDI'11 slides(pptx), PLDI'11 slides(pdf), ACM, PLDI'11, JavaMOP, BIB
Mining Parametric Specifications
Blank.gifChoonghwan Lee, Feng Chen and Grigore Rosu
Blank.gifICSE'11, ACM, pp 591-600. 2011
Blank.gifPDF, Slides(pptx), ACM, ICSE'11, jMiner, BIB
An Overview of the MOP Runtime Verification Framework
Blank.gifPatrick Meredith, Dongyun Jin, Dennis Griffith, Feng Chen and Grigore Rosu
Blank.gifJ.STTT, http://dx.doi.org/10.1007/s10009-011-0198-6
Blank.gifPDF, J.STTT, BIB

2011(NEW)

Maximal Causal Models for Sequentially Consistent Systems
Blank.gifTraian Florin Serbanuta and Feng Chen and Grigore Rosu
Blank.gifTechnical Report http://hdl.handle.net/2142/27708, October 2011
Blank.gifPDF, JPredictor, DOI, BIB
Improved Multithreaded Unit Testing
Blank.gifVilas Jagannath and Milos Gligoric and Dongyun Jin and Qingzhou Luo and Grigore Rosu and Darko Marinov
Blank.gifFSE'11, ACM, pp 223-233. 2011
Blank.gifPDF, DOI, FSE'11, BIB
MatchC: A Matching Logic Reachability Verifier Using the K Framework
Blank.gifAndrei Stefanescu
Blank.gifK'11, ENTCS 304. 2011
Blank.gifPDF, Matching Logic, DOI, BIB
The Rewriting Logic Semantics Project: A Progress Report
Blank.gifJose Meseguer and Grigore Rosu
Blank.gifFCT'11, Lecture Notes in Computer Science 6914, pp 1-37. 2011
Blank.gifPDF, K, DOI, FCT'11, BIB
An Executable Formal Semantics of C with Applications
Blank.gifChucky Ellison and Grigore Rosu
Blank.gifTechnical Report http://hdl.handle.net/2142/25816, July 2011
Blank.gifPDF, C Semantics, DOI, BIB
Towards Semantics-Based WCET Analysis
Blank.gifMihail Asavoae and Dorel Lucanu and Grigore Rosu
Blank.gifWCET'11. 2011
Blank.gifPDF, Slides(PDF), Matching Logic, WCET'11, BIB
Garbage Collection for Monitoring Parametric Properties
Blank.gifDongyun Jin and Patrick O'Neil Meredith and Dennis Griffith and Grigore Rosu
Blank.gifPLDI'11, ACM, pp 415-424. 2011
Blank.gifPDF, Slides(PPTX), Slides(PDF), MOP, DOI, PLDI'11, BIB
An Overview of the MOP Runtime Verification Framework
Blank.gifPatrick O'Neil Meredith and Dongyun Jin and Dennis Griffith and Feng Chen and Grigore Rosu
Blank.gifJ.STTT, Volume 14(3), pp 249-289. 2011
Blank.gifPDF, MOP, DOI, J.STTT, BIB
Matching Logic: A New Program Verification Approach (NIER Track)
Blank.gifGrigore Rosu and Andrei Stefanescu
Blank.gifICSE'11, ACM, pp 868-871. 2011
Blank.gifPDF, Slides(PPTX), Slides(PDF), Matching Logic, DOI, ICSE'11, BIB
Mining Parametric Specifications
Blank.gifChoonghwan Lee and Feng Chen and Grigore Rosu
Blank.gifICSE'11, ACM, pp 591-600. 2011
Blank.gifPDF, Slides(PPTX), JMiner, DOI, ICSE'11, BIB

2010

On Compiling Rewriting Logic Language Definitions into Competitive Interpreters
Blank.gifMichael Ilseman, Chucky Ellison and Grigore Rosu
Blank.gifTechnical Report http://hdl.handle.net/2142/17444, December 2010
Blank.gifPDF, TR@UIUC, Compiler Webpage, BIB
A Rewriting Approach to Concurrent Programming Language Design and Semantics
Blank.gifTraian Florin Serbanuta
Blank.gifPhD Thesis, University of Illinois, December 2010
Blank.gifPDF, Slides (PDF), K-Maude, TR@UIUC, BIB
Matching Logic: A New Program Verification Approach
Blank.gifGrigore Rosu and Andrei Stefanescu
Blank.gifUV'10. 2010
Blank.gifPDF, Slides(pptx), Slides(pdf), Matching Logic, K framework, UV'10, BIB
Runtime Verification with the RV System
Blank.gifPatrick Meredith and Grigore Rosu
Blank.gifRV'10, LNCS 6418, pp 136-152. 2010
Blank.gifPDF, Slides(PDF), Slides(PPT), Slides(KEY), RV'10, BIB
Automating Coinduction with Case Analysis
Blank.gifEugen-Ioan Goriac, Dorel Lucanu and Grigore Rosu
Blank.gifICFEM'10, LNCS 6447, pp 220-236. 2010
Blank.gifPDF, LNCS, ICFEM'10, CIRC, BIB
A Formal Executable Semantics of Verilog
Blank.gifPatrick Meredith, Michael Katelman, Jose Meseguer and Grigore Rosu
Blank.gifTechnical Report http://hdl.handle.net/2142/17079, July 2010
Blank.gifPDF, TR@UIUC, BIB
Matching Logic: An Alternative to Hoare/Floyd Logic
Blank.gifGrigore Rosu, Chucky Ellison and Wolfram Schulte
Blank.gifAMAST'10, LNCS 6486, pp 142-162. 2010
Blank.gifPDF, Slides(PPT), Slides(PDF), LNCS, AMAST'10, BIB
K-Maude: A Rewriting Based Tool for Semantics of Programming Languages
Blank.gifTraian Florin Serbanuta and Grigore Rosu
Blank.gifWRLA'10, LNCS 6381, pp 104-122. 2010
Blank.gifPDF, Slides (PDF), K-Maude, LNCS, WRLA'10, BIB
Ambient intelligence in self-organising assembly systems using the chemical reaction model
Blank.gifRegina Frei, Giovanna Di Marzo Serugendo and Traian Florin Serbanuta
Blank.gifJ. of Ambient Intelligence and Humanized Computing, Volume 1(3), pp 163-184. 2010
Blank.gifJ.AIHC, BIB
An Overview of the K Semantic Framework
Blank.gifGrigore Rosu and Traian Florin Serbanuta
Blank.gifJ.LAP, Volume 79(6), pp 397-434. 2010
Blank.gifPDF, Slides(PPTX), Slides(PDF), K Tool, J.LAP, BIB
A Formal Executable Semantics of Verilog
Blank.gifPatrick Meredith, Michael Katelman, Jose Meseguer and Grigore Rosu
Blank.gifMEMOCODE'10, IEEE, pp 179-188. 2010
Blank.gifPDF, Slides(PDF), Sources, Verilog Semantics, IEEE, MEMOCODE'10, BIB
IMUnit: Improved Multithreaded Unit Testing
Blank.gifVilas Jagannath, Milos Gligoric, Dongyun Jin, Grigore Rosu and Darko Marinov
Blank.gifIWMSE'10, IEEE, pp 48-49. 2010
Blank.gifPDF, IEEE, IWMSE'10, BIB
Efficient Monitoring of Parametric Context-Free Patterns
Blank.gifPatrick Meredith, Dongyun Jin, Feng Chen and Grigore Rosu
Blank.gifJ. of ASE, Volume 17(2), pp 149-180. 2010
Blank.gifPDF, J.ASE, BIB

2009

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

2008

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

2007

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

2006

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

2005

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

2005(NEW)

Monitoring Algorithms for Metric Temporal Logic
Blank.gifPrasanna Thati and Grigore Rosu
Blank.gifRV'05, Electronic Notes in Theoretical Computer Science 113, pp 145-162. 2005
Blank.gifPDF, MOP, DOI, RV'05, BIB
Rewriting-Based Techniques for Runtime Verification
Blank.gifGrigore Rosu and Klaus Havelund
Blank.gifJ.ASE, Volume 12(2), pp 151-197. 2005
Blank.gifPDF, MOP, DOI, J.ASE, BIB

2004

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

2003

CS322 - Programming Language Design: Lecture Notes
Blank.gifGrigore Rosu
Blank.gifTechnical Report http://hdl.handle.net/2142/11385, December 2003
Blank.gifPDF, Matching Logic, DOI, BIB
Generating Optimal Linear Temporal Logic Monitors by Coinduction
Blank.gifKoushik Sen and Grigore Rosu and Gul Agha
Blank.gifASIAN'03, Lecture Notes in Computer Science (LNCS) 2896, pp 260-275. 2003
Blank.gifPDF, MOP, DOI, ASIAN'03, BIB
Certifying Measurement Unit Safety Policy
Blank.gifGrigore Rosu and Feng Chen
Blank.gifASE'03, IEEE, pp 304-309. 2003
Blank.gifPDF, MOP, DOI, ASE'03, BIB
Certifying and Synthesizing Membership Equational Proofs
Blank.gifGrigore Rosu and Steven Eker and Patrick Lincoln and Jose Meseguer
Blank.gifFME'03, Lecture Notes in Computer Science (LNCS) 2805, pp 359-380. 2003
Blank.gifPDF, Slides(PPT), Maude, DOI, FME'03, BIB
Generating Optimal Monitors for Extended Regular Expressions
Blank.gifKoushik Sen and Grigore Rosu
Blank.gifRV'03, Electronic Notes in Theoretical Computer Science 89(2), pp 226-245. 2003
Blank.gifPDF, MOP, DOI, RV'03, BIB
Testing Extended Regular Language Membership Incrementally by Rewriting
Blank.gifGrigore Rosu and Mahesh Viswanathan
Blank.gifRTA'03, Lecture Notes in Computer Science (LNCS) 2706, pp 499-514. 2003
Blank.gifPDF, Slides(PPT), MOP, DOI, RTA'03, BIB
Rule-Based Analysis of Dimensional Safety
Blank.gifFeng Chen and Grigore Rosu and Ram prasad Venkatesan
Blank.gifRTA'03, Lecture Notes in Computer Science (LNCS) 2706, pp 197-207. 2003
Blank.gifPDF, MOP, DOI, RTA'03, BIB
Towards Monitoring-Oriented Programming: A Paradigm Combining Specification and Implementation
Blank.gifFeng Chen and Grigore Rosu
Blank.gifRV'03, Electronic Notes in Theoretical Computer Science 89(2), pp 108-127. 2003
Blank.gifPDF, MOP, DOI, RV'03, BIB
Inductive Behavioral Proofs by Unhiding
Blank.gifGrigore Rosu
Blank.gifCMCS'03, Volume 82(1), pp 285-302. 2003
Blank.gifPDF, Logic, DOI, CMCS'03, BIB

Retrieved from "http://fsl.cs.illinois.edu/index.php?title=FSL_Publications&oldid=17885"
Personal tools
Namespaces

Variants
Actions
Navigation