Difference between revisions of "Grigore Rosu's Publications"

From FSL

Jump to: navigation, search

Revision as of 10:15, 16 September 2018

(back to Grigore Rosu's page)

This list contains only my newer publications. See DBLP and my old publication page for the remaining papers.

2018

A Language-Independent Program Verification Framework

Xiaohong Chen and Grigore Rosu

ISoLA'18, Springer, pp 92-102. 2018

PDF, Slides(PPTX), DOI, ISoLA'18, BIB

A Language-Independent Approach to Smart Contract Verification

Xiaohong Chen and Daejun Park and Grigore Rosu

ISoLA'18, Springer, pp 405-413. 2018

PDF, Slides(PPTX), Formally Verified Smart Contracts, DOI, ISoLA'18, BIB

A Formal Verification Tool for Ethereum VM Bytecode

Daejun Park and Yi Zhang and Manasvi Saxena and Philip Daian and Grigore Rosu

ESEC/FSE'18, ACM, pp 912-915. 2018

PDF, Slides(PDF), Formally Verified Smart Contracts, DOI, ESEC/FSE'18, BIB

IELE: An Intermediate-Level Blockchain Language Designed and Implemented Using Formal Semantics

Theodoros Kasampalis and Dwight Guth and Brandon Moore and Traian Serbanuta and Virgil Serbanuta and Daniele Filaretti and Grigore Rosu and Ralph Johnson

Technical Report http://hdl.handle.net/2142/100320, July 2018

PDF, IELE, DOI, BIB

Program Verification by Coinduction

Brandon Moore and Lucas Pena and Grigore Rosu

ESOP'18, Springer, pp 589-618. 2018

PDF, Matching Logic, DOI, ESOP'18, BIB

P4K: A Formal Semantics of P4 and Applications

Ali Kheradmand and Grigore Rosu

Technical Report https://arxiv.org/abs/1804.01468, April 2018

PDF, P4K, DOI, BIB

KEVM: A Complete Semantics of the Ethereum Virtual Machine

Everett Hildenbrandt and Manasvi Saxena and Xiaoran Zhu and Nishant Rodrigues and Philip Daian and Dwight Guth and Brandon Moore and Yi Zhang and Daejun Park and Andrei Stefanescu and Grigore Rosu

CSF 2018, IEEE, pp 204-217. 2018

PDF, KEVM, CSF 2018, BIB

2017

Matching logic

LMCS, Volume 13(4), pp 1-61. 2017

PDF, project, DOI, LMCS, BIB

Open Problems and Challenges 2017

Technical Report http://hdl.handle.net/2142/95775, March 2017

PDF, Webpage, DOI, BIB

K - A Semantic Framework for Programming Languages and Formal Analysis Tools

Marktoberdorf'16, NATO Science for Peace and Security. 2017. To appear

2016

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

Finite-Trace Linear Temporal Logic: Coinductive Completeness

RV'16, LNCS 10012, pp 333-350. 2016

PDF, Slides(PPTX), Matching Logic, DOI, RV'16, BIB

Runtime Verification at Work: A Tutorial

Philip Daian and Dwight Guth and Chris Hathhorn and Yilong Li and Edgar Pek and Manasvi Saxena and Traian Florin Serbanuta and Grigore Rosu

RV'16, LNCS 10012, pp 46-67. 2016

PDF, 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

Owolabi Legunsen and Wajih Ul Hassan and Xinyue Xu and Grigore Rosu and Darko Marinov

ASE 2016, IEEE/ACM, pp 602-613. 2016

PDF, Slides(PDF), JavaMOP, DOI, ASE 2016, 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

RV-ECU: Maximum Assurance In-Vehicle Safety Monitoring

Philip Daian and Bhargava Manja and Shinichi Shiraishi and Akihito Iwai and Grigore Rosu

SAE'16, SAE International 2016-01-0126, pp 1-13. 2016

PDF, Slides(PPT), RV-ECU, DOI, SAE'16, BIB

Open Problems and Challenges 2016

Technical Report http://hdl.handle.net/2142/88925, February 2016

PDF, Webpage, DOI, BIB

Language Definitions as Rewrite Theories

Vlad Rusu and Dorel Lucanu and Traian Florin Serbanuta and Andrei Arusoaie and Andrei Stefanescu and Grigore Rosu

J.LAMP, Volume 85(1, Part 1), pp 98-120. 2016

PDF, project, DOI, J.LAMP, 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

2015

From Rewriting Logic, to Programming Language Semantics, to Program Verification

Meseguer's Festschrift, LNCS 9200, pp 598-616. 2015

PDF, Slides(PPTX), K, DOI, Meseguer's Festschrift, BIB

RV-Android: Efficient Parametric Android Runtime Verification, a Brief Tutorial

Philip Daian and Ylies Falcone and Patrick Meredith and Traian Florin Serbanuta and Shinichi Shiraishi and Akihito Iwai and Grigore Rosu

RV'15, Lecture Notes in Computer Science 9333, pp 342-357. 2015

PDF, Slides(PDF), RV-Android, DOI, RV'15, BIB

Matching Logic --- Extended Abstract

RTA'15, Leibniz International Proceedings in Informatics (LIPIcs) 36, pp 5-21. 2015

PDF, Slides(PPTX), Matching Logic, DOI, RTA'15, 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

GPredict: Generic Predictive Concurrency Analysis

Jeff Huang and Qingzhou Luo and Grigore Rosu

ICSE'15, ACM, pp 847-857. 2015

PDF, Slides(PDF), jPredictor, DOI, ICSE'15, BIB

Evolution-Aware Monitoring-Oriented Programming

Owolabi Legunsen and Darko Marinov and Grigore Rosu

ICSE NIER'15, ACM, pp 615-618. 2015

PDF, Slides(PDF), JavaMOP, DOI, ICSE NIER'15, BIB

Term-Generic Logic

Andrei Popescu and Grigore Rosu

Journal of Theoretical Computer Science, Volume 577(1), pp 1-24. 2015

PDF, project, DOI, Journal of Theoretical Computer Science, BIB

Program Verification by Coinduction

Brandon Moore and Grigore Rosu

Technical Report http://hdl.handle.net/2142/73177, February 2015

PDF, Matching Logic, DOI, 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

2014

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

ROSRV: Runtime Verification for Robots

Jeff Huang and Cansu Erdogan and Yi Zhang and Brandon Moore and Qingzhou Luo and Aravind Sundaresan and Grigore Rosu

RV'14, LNCS 8734, pp 247-254. 2014

PDF, Slides(PPTX), Slides(PDF), ROSRV, DOI, RV'14, BIB

RV-Monitor: Efficient Parametric Runtime Verification with Simultaneous Properties

Qingzhou Luo and Yi Zhang and Choonghwan Lee and Dongyun Jin and Patrick O'Neil Meredith and Traian Florin Serbanuta and Grigore Rosu

RV'14, LNCS 8734, pp 285-300. 2014

PDF, Slides(PPTX), JavaMOP, DOI, RV'14, BIB

All-Path Reachability Logic

Andrei Stefanescu and Stefan Ciobaca and Radu Mereuta and Brandon Moore and Traian Florin Serbanuta and Grigore Rosu

RTA'14, LNCS 8560, pp 425-440. 2014

PDF, Slides(PPTX), Matching Logic, DOI, RTA'14, BIB

Maximal Sound Predictive Race Detection with Control Flow Abstraction

Jeff Huang and Patrick Meredith and Grigore Rosu

PLDI'14, ACM, pp 337-348. 2014

PDF, Slides(PPT), Slides(PDF), jPredictor, DOI, PLDI'14, BIB

On the Complexity of Stream Equality

Joerg Endrullis and Dimitri Hendriks and Rena Bakhshi and Grigore Rosu

Journal of Functional Programming, Volume 24(2-3), pp 166-217. 2014

PDF, CIRC, DOI, Journal of Functional Programming, BIB

Language Definitions as Rewrite Theories

Andrei Arusoaie and Dorel Lucanu and Vlad Rusu and Traian Florin Serbanuta and Andrei Stefanescu and Grigore Rosu

WRLA'14, LNCS 8663, pp 97-112. 2014

PDF, K, DOI, WRLA'14, BIB

Behavioral Rewrite Systems and Behavioral Productivity

Grigore Rosu and Dorel Lucanu

Futatsugi Festschrift 2014, LNCS 8373, pp 296-314. 2014

PDF, Slides(PPTX), CIRC, DOI, Futatsugi Festschrift 2014, BIB

Matching Logic: A Logic for Structural Reasoning

Technical Report http://hdl.handle.net/2142/47004, Jan 2014

PDF, Matching Logic, DOI, BIB

2013

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

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

SYNASC'13, IEEE/CPS, pp 28-31. 2013

PDF, Slides(PPTX), K, DOI, SYNASC'13, BIB

EnforceMOP: A Runtime Property Enforcement System for Multithreaded Programs

Qingzhou Luo and Grigore Rosu

ISSTA'13, ACM, pp 156-166. 2013

PDF, Slides(PPTX), EnforceMOP, DOI, ISSTA'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

Low-Level Program Verification using Matching Logic Reachability

Dwight Guth and Andrei Stefanescu and Grigore Rosu

LOLA'13. 2013

PDF, Slides(PDF), Matching Logic, LOLA'13, BIB

Efficient Parametric Runtime Verification with Deterministic String Rewriting

Patrick Meredith and Grigore Rosu

ASE'13, IEEE/ACM, pp 70-80. 2013

PDF, Slides(PPT), Slides(KEY), Slides(PDF), MOP, DOI, ASE'13, BIB

2012

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

Maximal Causal Models for Sequentially Consistent Systems

Traian Florin Serbanuta, Feng Chen and Grigore Rosu

RV'12, LNCS. 7687, pp 136-150. 2013

PDF, 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

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, , BIB

Security-Policy Monitoring and Enforcement with JavaMOP

Soha Hussein, Patrick Meredith and Grigore Rosu

PLAS'12, ACM, pp 3:1-3:11. 2012

PDF, Slides(KEY), Slides(PDF), ACM, PLAS'12, 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

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

Defining the Undefinedness of C

Chucky Ellison and Grigore Rosu

Technical Report http://hdl.handle.net/2142/30780, April 2012

PDF, TR@UIUC, BIB

Scalable Parametric Runtime Monitoring

Dongyun Jin, Patrick Meredith and Grigore Rosu

Technical Report http://hdl.handle.net/2142/30757, April 2012

PDF, TR@UIUC, BIB

Efficient Parametric Runtime Verification with Deterministic String Rewriting

Patrick Meredith and Grigore Rosu

Technical Report http://www.ideals.illinois.edu/handle/2142/30467, March 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

JavaMOP: Efficient Parametric Runtime Monitoring Framework

Dongyun Jin, Patrick Meredith, Choonghwan Lee and Grigore Rosu

ICSE'12, IEEE, pp 1427-1430. 2012

PDF, Demo Movie, TOOL ICSE'12, BIB

Towards Categorizing and Formalizing the JDK API

Choonghwan Lee, Dongyun Jin, Patrick Meredith and Grigore Rosu

Technical Report http://hdl.handle.net/2142/30006, March 2012

PDF, TR@UIUC, BIB

Semantics and Algorithms for Parametric Monitoring

Grigore Rosu and Feng Chen

J.LMCS, Volume 8(1), pp 1-47. 2012

PDF, MOP, J.LMCS, 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

2011

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

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

Improved Multithreaded Unit Testing

Vilas Jagannath, Milos Gligoric, Dongyun Jin, Qingzhou Luo, Grigore Rosu and Darko Marinov

FSE'11, ACM, pp 223-233. 2011

PDF, FSE'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

Garbage Collection for Monitoring Parametric Properties

Dongyun Jin, Patrick Meredith, Dennis Griffith and Grigore Rosu

PLDI'11, ACM, pp 415-424. 2011

PDF, PLDI'11 slides(pptx), PLDI'11 slides(pdf), ACM, PLDI'11, JavaMOP, BIB

Mining Parametric Specifications

Choonghwan Lee, Feng Chen and Grigore Rosu

ICSE'11, ACM, pp 591-600. 2011

PDF, Slides(pptx), ACM, ICSE'11, jMiner, BIB

An Overview of the MOP Runtime Verification Framework

Patrick Meredith, Dongyun Jin, Dennis Griffith, Feng Chen and Grigore Rosu

J.STTT, http://dx.doi.org/10.1007/s10009-011-0198-6

PDF, J.STTT, BIB

Maximal Causal Models for Sequentially Consistent Systems

Traian Florin Serbanuta and Feng Chen and Grigore Rosu

Technical Report http://hdl.handle.net/2142/27708, October 2011

PDF, JPredictor, DOI, BIB

Improved Multithreaded Unit Testing

Vilas Jagannath and Milos Gligoric and Dongyun Jin and Qingzhou Luo and Grigore Rosu and Darko Marinov

FSE'11, ACM, pp 223-233. 2011

PDF, DOI, FSE'11, 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

Garbage Collection for Monitoring Parametric Properties

Dongyun Jin and Patrick O'Neil Meredith and Dennis Griffith and Grigore Rosu

PLDI'11, ACM, pp 415-424. 2011

PDF, Slides(PPTX), Slides(PDF), MOP, DOI, PLDI'11, BIB

An Overview of the MOP Runtime Verification Framework

Patrick O'Neil Meredith and Dongyun Jin and Dennis Griffith and Feng Chen and Grigore Rosu

J.STTT, Volume 14(3), pp 249-289. 2011

PDF, MOP, DOI, J.STTT, 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

Mining Parametric Specifications

Choonghwan Lee and Feng Chen and Grigore Rosu

ICSE'11, ACM, pp 591-600. 2011

PDF, Slides(PPTX), JMiner, DOI, ICSE'11, BIB

2010

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

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

Runtime Verification with the RV System

Patrick Meredith and Grigore Rosu

RV'10, LNCS 6418, pp 136-152. 2010

PDF, Slides(PDF), Slides(PPT), Slides(KEY), RV'10, 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

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

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

IMUnit: Improved Multithreaded Unit Testing

Vilas Jagannath, Milos Gligoric, Dongyun Jin, Grigore Rosu and Darko Marinov

IWMSE'10, IEEE, pp 48-49. 2010

PDF, IEEE, IWMSE'10, BIB

Efficient Monitoring of Parametric Context-Free Patterns

Patrick Meredith, Dongyun Jin, Feng Chen and Grigore Rosu

J. of ASE, Volume 17(2), pp 149-180. 2010

PDF, J.ASE, BIB

2009

Efficient Formalism-Independent Monitoring of Parametric Properties

Feng Chen, Patrick Meredith, Dongyun Jin and Grigore Rosu

ASE'09, IEEE/ACM, pp 383-394. 2009

PDF, ASE'09 slides(KEY), ASE'09 slides(PDF), IEEE, ASE'09, BIB

Circular Coinduction with Special Contexts

Dorel Lucanu and Grigore Rosu

ICFEM'09, LNCS 5885, pp 639-659. 2009

PDF, Slides(PDF), LNCS, ICFEM'09, 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

Circular Coinduction: A Proof Theoretical Foundation

Grigore Rosu and Dorel Lucanu

CALCO'09, LNCS 5728, pp 127-144. 2009

Slides (PDF), LNCS, CALCO'09, DBLP, 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

A Semantic Approach to Interpolation

Andrei Popescu, Traian Florin Serbanuta and Grigore Rosu

J. of TCS, Volume 410(12-13), pp 1109-1128. 2009

PDF, J.TCS, BIB

Monitoring Oriented Programming - A Project Overview

Feng Chen, Dongyun Jin, Patrick Meredith, and Grigore Rosu

ICICIS'09, pp 72-77. 2009

PDF, ICICIS'09, BIB

A Rewriting Logic Approach to Operational Semantics

Traian Florin Serbanuta, Grigore Rosu and Jose Meseguer

Information and Computation, Volume 207(2), pp 305-340. 2009

PDF, Experiments, J.Inf.&Comp., BIB

Parametric Trace Slicing and Monitoring

Feng Chen and Grigore Rosu

TACAS'09, LNCS 5505, pp 246-261. 2009.

PDF, Slides (PPT), LNCS, TACAS'09, DBLP, BIB

Dependent advice: A general approach to optimizing history-based Aspects

Eric Bodden, Feng Chen and Grigore Rosu

AOSD'09, ACM, pp 3--14. 2009.

PDF, ACM, AOSD'09, TR@ABC, BIB

2008

Towards a Module System for K

Mark Hills and Grigore Rosu

WADT'08, LNCS 5486, pp 187-205. 2009

PDF, LNCS, WADT'08, BIB

Term-Generic Logic

Andrei Popescu and Grigore Rosu

WADT'08, LNCS 5486, pp 290-307. 2009

LNCS, WADT'08, BIB

Hardware Runtime Monitoring for Dependable COTS-based Real-Time Embedded Systems

Rodolfo Pellizzoni, Patrick Meredith, Marco Caccamo and Grigore Rosu

RTSS'08, IEEE, pp. 481-491. 2008

PDF, Experiments, Slides(PPTX), IEEE, RTSS'08, BIB

Deﬁning 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

Efficient Monitoring of Parametric Context-Free Patterns

Patrick Meredith, Dongyun Jin, Feng Chen and Grigore Rosu

ASE'08, IEEE/ACM, pp 148-157. 2008 ACM Sigsoft Distinguished Paper

PDF, Experiments, ASE'08 slides(KEY), ASE'08 slides(MOV), ASE'08 slides(PPT), IEEE, ASE'08, BIB

Mining Parametric State-Based Specifications from Executions

Feng Chen and Grigore Rosu

Technical report UIUCDCS-R-2008-3000, September 2008

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

Monitoring IVHM Systems using a Monitor-Oriented Programming Framework

Sudipto Ghoshal, Solaiappan Manimaran, Grigore Rosu, Traian Florin Serbanuta, and Gheorghe Stefanescu

LFM 2008

PDF, Slides (PPT), LFM'08, BIB

jPredictor: A Predictive Runtime Analysis Tool for Java

Feng Chen and Traian Florin Serbanuta and Grigore Rosu

ICSE'08, ACM, pp. 221-230. 2008

PDF, Slides(PDF), DOI, ICSE'08, 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

Synthesizing Monitors for Safety Properties -- This Time With Calls and Returns --

Grigore Rosu, Feng Chen and Thomas Ball

RV'08, LNCS 5289, pp 51-68, 2008

PDF, RV'08, BIB

Pluggable Policies for C

Mark Hills, Feng Chen and Grigore Rosu

Technical Report UIUCDCS-R-2008-2931, January 2008

PDF, TR@UIUC, BIB

2007

K: A Rewriting-Based Framework for Computations -- Preliminary version

Technical report UIUCDCS-R-2007-2926 and UILU-ENG-2007-1827, December 2007

PDF, ZIP, TR@UIUC, BIB

Synthesizing Monitors for Safety Properties -- This Time With Calls and Returns --

Grigore Rosu,Feng Chen and Thomas Ball

Technical report UIUCDCS-R-2007-2908, October 2007

A K Definition of Scheme

Patrick Meredith, Mark Hills and Grigore Rosu

Technical Report UIUCDCS-R-2007-2907, October 2007

PDF, TR@UIUC, BIB

Effective Predictive Runtime Analysis Using Sliced Causality and Atomicity

Feng Chen, Traian Florin Serbanuta and Grigore Rosu

Technical report UIUCDCS-R-2007-2905, 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

MOP: An Efficient and Generic Runtime Verification Framework

Feng Chen and Grigore Rosu

OOPSLA'07, ACM press, pp 569-588. 2007

PDF, OOPSLA'07 slides, ACM, OOPSLA'07, DBLP, TR@UIUC, 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

CIRC: A Circular Coinductive Prover

Dorel Lucanu and Grigore Rosu

CALCO'07, LNCS 4624, pp 372-378. 2007

PDF, CIRC webpage, CALCO'07, BIB

Parametric and Sliced Causality

Feng Chen and Grigore Rosu

CAV'07, LNCS 4590, pp 240 - 253, 2007

PDF, CAV'07 slides, CAV'07, TR@UIUC, 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

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 Safety Properties and Their Monitoring

Technical report UIUCDCS-R-2007-2850, February 2007

PDF, ZIP, TR@UIUC, BIB

An Effective Algorithm for the Membership Problem for Extended Regular Expressions

FOSSACS'07, LNCS 4423, pp 332-345, 2007

PDF, FOSSACS'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

2006

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

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

MOP: Reliable Software Development using Abstract Aspects

Feng Chen and Grigore Rosu

Technical report UIUCDCS-R-2006-2776, October 2006

PDF, TR@UIUC, BIB

Computationally Equivalent Elimination of Conditions - extended abstract

Traian Florin Serbanuta and Grigore Rosu

RTA'06, LNCS 4098, pp 19-34. 2006

PDF, Slides (PPT), Experiments, LNCS, RTA'06, DBLP, BIB

GFOL: a Term-Generic Logic for Defining Lambda-Calculi

Andrei Popescu and Grigore Rosu

Technical Report UIUCDCS-R-2006-2756, July 2006

PDF, TR@UIUC, BIB

Equality of Streams is a Pi_2^0-Complete Problem

ICFP'06, ACM, 2006

PDF, ICFP'06 Slides, ACM, ICFP'06, BIB

Complete Categorical Deduction for Satisfaction as Injectivity

Festschrift in Honor of Joseph Goguen, LNCS 4060, pp 157-172. 2006.

PDF, Goguen's Festschrift slides, LNCS, Goguen's Festschrift, Goguen's Webpage, BIB

Allen Linear (Interval) Temporal Logic -Translation to LTL and Monitor Synthesis-

Grigore Rosu and Saddek Bensalem

CAV'06, LNCS 4144, pp 263-277, 2006

PDF, CAV'06, CAV'06 Slides, BIB

Parametric and Termination-Sensitive Control Dependence - Extended Abstract

Feng Chen and Grigore Rosu

SAS'06, LNCS 4134, pp 387-404. 2006.

PDF, LNCS, SAS'06, BIB

Parametric and Termination-Sensitive Control Dependence

Feng Chen and Grigore Rosu

Technical report UIUCDCS-R-2006-2712, April 2006

PDF, TR@UIUC, BIB

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

Predicting Concurrency Errors at Runtime using Sliced Causality

Feng Chen and Grigore Rosu

Technical report UIUCDCS-R-2006-2965, 2006.

PDF, TR@UIUC, BIB

A Semantic Approach to Interpolation

Andrei Popescu, Traian Florin Serbanuta and Grigore Rosu

FOSSACS'06, LNCS 3921, pp 307-321. 2006

PDF, Slides (PDF), LNCS, FOSSACS '06, DBLP, BIB

Static Analysis to Enforce Safe Value Flow in Embedded Control Systems

Sumant Kowshik, Grigore Rosu and Lui Sha

DSN'06, IEEE, pp 23-34. 2006.

PDF, DSN'06 Slides, IEEE, DSN'06, BIB

2005

Efficient Monitoring of Omega-Languages

Marcelo d'Amorim and Grigore Rosu

CAV'05, LNCS 3576, pp 364 - 378. 2005.

PDF, LNCS, CAV'05, DBLP, BIB

Behavioral Extensions of Institutions

Andrei Popescu and Grigore Rosu

CALCO'05, LNCS 3629, pp. 331-347. 2005

PDF, CALCO'05 Slides, LNCS , CALCO '05, DBLP, BIB

Predicting Concurrency Errors at Runtime using Sliced Causality

Feng Chen and Grigore Rosu

Technical report UIUCDCS-R-2005-2660, 2005.

PDF, TR@UIUC, BIB

Checking and Correcting Behaviors of Java Programs at Runtime with Java-MOP

Feng Chen, Marcelo d'Amorim and Grigore Rosu

RV'05, ENTCS 144, issue 4, pp 3-20. 2005.

PDF, ENTCS, RV'05, DBLP, BIB

Java-MOP: A Monitoring Oriented Programming Environment for Java

Feng Chen and Grigore Rosu

TACAS'05, LNCS 3440, pp 546-550. 2005.

PDF, LNCS, TACAS'05, DBLP, BIB

Automatic and Precise Dimensional Analysis

Marcelo d'Amorim, Mark Hills, Feng Chen and Grigore Rosu

Technical Report UIUCDCS-R-2005-2668, December 2005

PDF, Sources, TR@UIUC, BIB

K: a Rewrite-based Framework for Modular Language Design, Semantics, Analysis and Implementation

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

Rewriting-based Techniques for Runtime Verification

Grigore Rosu and Klaus Havelund

J.ASE, Volume 12(2), pp 151-197. 2005

PDF, J.ASE, DBLP, BIB

The Rewriting Logic Semantics Project

Jose Meseguer and Grigore Rosu

SOS'05, ENTCS 156, pp. 27-56. 2006

PDF, SOS'05, BIB

An Effective Algorithm for the Membership Problem for Extended Regular Expressions

Technical Report UIUCDCS-R-2005-2694, August 2005

PDF, Technical Report @ UIUC, BIB

Monitoring Algorithms for Metric Temporal Logic

Prasanna Thati and Grigore Rosu

RV'05, Electronic Notes in Theoretical Computer Science 113, pp 145-162. 2005

PDF, MOP, DOI, RV'05, BIB

Rewriting-Based Techniques for Runtime Verification

Grigore Rosu and Klaus Havelund

J.ASE, Volume 12(2), pp 151-197. 2005

PDF, MOP, DOI, J.ASE, BIB

2004

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

Efficient Monitoring of Safety Properties

Klaus Havelund and Grigore Rosu

J. of STTT, Volume 6(2), pp 158-173. 2004

PDF, J.STTT, BIB

A Formal Monitoring-based Framework for Software Development and Analysis

Feng Chen and Marcelo d'Amorim and Grigore Rosu

ICFEM'04, LNCS 3308, pp 357 - 373. 2004.

PDF, LNCS, ICFEM'04, DBLP, BIB

Monitoring-Oriented Programming: A Tool-Supported Methodology for Higher Quality Object-Oriented Software

Feng Chen, Marcelo d'Amorim and Grigore Rosu

Technical Report UIUCDCS-R-2004-2420, 2004.

PDF, TR@UIUC, 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

From Conditional to Unconditional Rewriting

WADT'04, LNCS 3423, pp 218-233. 2004

PDF, LNCS, WADT'04, Experiments, PDF - Original submission, WADT'04 slides, BIB

From Conditional to Unconditional Rewriting

Technical Report UIUCDCS-R-2004-2471, August 2004

PDF, Technical reports' page, Experiments, BIB

Behavioral Abstraction is Hiding Information

J. of TCS, Volume 327(1-2), pp 197-221. 2004

PDF, J.TCS, BIB

2003

Certifying Measurement Unit Safety Policy

Grigore Rosu and Feng Chen

ASE'03, IEEE, pp. 304 - 309. 2003.

PDF, IEEE, ASE'03, BIB

Rule-Based Analysis of Dimensional Safety

Feng Chen and Grigore Rosu and Ram Prasad Venkatesan

RTA'03, LNCS 2706, pp197 - 207. 2003.

PDF, LNCS, RTA'03, DBLP, BIB

Towards Monitoring-Oriented Programming: A Paradigm Combining Specification and Implementation

Feng Chen and Grigore Rosu

RV'03, ENTCS 89, issue 2, pp 108 - 127. 2003.

PDF, ENTCS, RV'03, DBLP, BIB

CS322 - Programming Language Design: Lecture Notes

Technical Report UIUCDCS-R-2003-2897, December 2003

PDF, TR @ UIUC, BIB

Inductive Behavioral Proofs by Unhiding

CMCS'03, ENTCS 82(1). 2003

PDF, ENTCS, CMCS'03, Experiments, DBLP, BIB

CS322 - Programming Language Design: Lecture Notes

Technical Report http://hdl.handle.net/2142/11385, December 2003

PDF, Matching Logic, DOI, BIB

Generating Optimal Linear Temporal Logic Monitors by Coinduction

Koushik Sen and Grigore Rosu and Gul Agha

ASIAN'03, Lecture Notes in Computer Science (LNCS) 2896, pp 260-275. 2003

PDF, MOP, DOI, ASIAN'03, BIB

Certifying Measurement Unit Safety Policy

Grigore Rosu and Feng Chen

ASE'03, IEEE, pp 304-309. 2003

PDF, MOP, DOI, ASE'03, BIB

Certifying and Synthesizing Membership Equational Proofs

Grigore Rosu and Steven Eker and Patrick Lincoln and Jose Meseguer

FME'03, Lecture Notes in Computer Science (LNCS) 2805, pp 359-380. 2003

PDF, Slides(PPT), Maude, DOI, FME'03, BIB

Generating Optimal Monitors for Extended Regular Expressions

Koushik Sen and Grigore Rosu

RV'03, Electronic Notes in Theoretical Computer Science 89(2), pp 226-245. 2003

PDF, MOP, DOI, RV'03, BIB

Testing Extended Regular Language Membership Incrementally by Rewriting

Grigore Rosu and Mahesh Viswanathan

RTA'03, Lecture Notes in Computer Science (LNCS) 2706, pp 499-514. 2003

PDF, Slides(PPT), MOP, DOI, RTA'03, BIB

Rule-Based Analysis of Dimensional Safety

Feng Chen and Grigore Rosu and Ram prasad Venkatesan

RTA'03, Lecture Notes in Computer Science (LNCS) 2706, pp 197-207. 2003

PDF, MOP, DOI, RTA'03, BIB

Towards Monitoring-Oriented Programming: A Paradigm Combining Specification and Implementation

Feng Chen and Grigore Rosu

RV'03, Electronic Notes in Theoretical Computer Science 89(2), pp 108-127. 2003

PDF, MOP, DOI, RV'03, BIB

Inductive Behavioral Proofs by Unhiding

CMCS'03, Volume 82(1), pp 285-302. 2003

PDF, Logic, DOI, CMCS'03, BIB

2002

Synthesizing Monitors for Safety Properties

Klaus Havelund and Grigore Rosu

TACAS'02, LNCS 2280, pp 342-356. 2002

PDF, Slides(PPT), MOP, DOI, TACAS'02, BIB

2001

Interpreting Abstract Interpretations in Membership Equational Logic

Bernd Fischer and Grigore Rosu

RULE'01, Electronic Notes in Theoretical Computer Science 59(4), pp 271-285. 2001

PDF, Maude, DOI, BIB

Certifying Domain-Specific Policies

Michael Lowry and Thomas Pressburger and Grigore Rosu

ASE'01, IEEE, pp 81-90. 2001

PDF, Slides(PPT), AutoFilter, DOI, ASE'01, BIB

Monitoring Programs using Rewriting

Klaus Havelund and Grigore Rosu

ASE'01, IEEE, pp 135-143. 2001

PDF, Slides(PPT), MOP, DOI, ASE'01, BIB

Synthesizing Dynamic Programming Algorithms from Linear Temporal Logic Formulae

Grigore Rosu and Klaus Havelund

Technical Report https://ti.arc.nasa.gov/m/pub-archive/archive/0220.pdf, January 2001

2000

Hidden Logic

PhD Thesis, University of California at San Diego

PDF, Thesis@UCSD, BIB

Abstract Semantics for Module Composition

Technical Report http://roger.ucsd.edu/record=b7304233~S9, May 2000

1999

1998

1997

1996

Retrieved from "http://fsl.cs.illinois.edu/index.php?title=Grigore_Rosu%27s_Publications&oldid=18595"

Personal tools

Log in