Publications

2024

• A Logical Treatment of Finite Automata

  Nishant Rodrigues and Mircea Sebe and Xiaohong Chen and Grigore Rosu
  TACAS'24 ACM, April 2024
  PDF BIB TACAS'24 Matching Logic in MM0

2023

• Generating Proof Certificates for a Language-Agnostic Deductive Program Verifier

  Zhengyao Lin and Xiaohong Chen and Minh-Thai Trinh and John Wang and Grigore Rosu
  OOPSLA'23 ACM, July 2023
  PDF BIB OOPSLA'23 Matching Logic Proof Checker

2021

• Towards a Trustworthy Semantics-Based Language Framework via Proof Generation

  Xiaohong Chen and Zhengyao Lin and Minh-Thai Trinh and Grigore Rosu
  CAV'21 ACM, July 2021
  PDF BIB CAV'21 Matching Logic Proof Checker

2020

• Towards A Unified Proof Framework for Automated Fixpoint Reasoning Using Matching Logic

  Xiaohong Chen and Minh-Thai Trinh and Nishant Rodrigues and Lucas Pena and Grigore Rosu
  OOPSLA'20 ACM/IEEE, pp 1-29, Nov 2020
  PDF BIB OOPSLA'20 Matching Logic

• Towards A Unified Proof Framework for Automated Fixpoint Reasoning Using Matching Logic

  Xiaohong Chen and Minh-Thai Trinh and Nishant Rodrigues and Lucas Pena and Grigore Rosu
  Technical Report September 2020 http://hdl.handle.net/2142/108369
  PDF BIB Matching Logic

• A General Approach to Define Binders Using Matching Logic

  Xiaohong Chen and Grigore Rosu
  ICFP'20 ACM/IEEE, Volume 4, pp 1-32, Aug 2020
  PDF BIB ICFP'20 Matching Logic DOI

• Matching Logic Explained

  Xiaohong Chen and Dorel Lucanu and Grigore Rosu
  Technical Report July 2020 http://hdl.handle.net/2142/107794
  PDF BIB Matching Logic

• Initial algebra semantics in matching logic

  Xiaohong Chen and Dorel Lucanu and Grigore Rosu
  Technical Report July 2020 http://hdl.handle.net/2142/107781
  PDF BIB Matching Logic

• A General Approach to Define Binders Using Matching Logic

  Xiaohong Chen and Grigore Rosu
  Technical Report June 2020 http://hdl.handle.net/2142/106608
  PDF BIB Matching Logic

• Formal Semantics of Hybrid Automata

  Manasvi Saxena and Nishant Rodrigues and Xiaohong Chen and Grigore Rosu
  Technical Report April 2020 http://hdl.handle.net/2142/106822
  PDF BIB Matching Logic

• Connecting Constrained Constructor Patterns and Matching Logic

  Xiaohong Chen and Dorel Lucanu and Grigore Rosu
  WRLA'20 April 2020
  PDF BIB WRLA'20 Matching Logic

2019

• IELE: A Rigorously Designed Language and Tool Ecosystem for the Blockchain

  Kasampalis, Theodoros and Guth, Dwight and Moore, Brandon and Serbanuta, Traian Florin and Zhang, Yi and Filaretti, Daniele and Serbanuta, Virgil and Johnson, Ralph and Rosu, Grigore
  FM 2019 pp 593-610, October 2019
  PDF BIB

• Applicative Matching Logic: Semantics of K

  Xiaohong Chen and Grigore Rosu
  Technical Report July 2019 http://hdl.handle.net/2142/104616
  PDF BIB Matching Logic

• A Complete Formal Semantics of x86-64 User-Level Instruction Set Architecture

  Sandeep Dasgupta and Daejun Park and Theodoros Kasampalis and Vikram S. Adve and Grigore Rosu
  PLDI'19 ACM, pp 1133-1148, June 2019
  PDF BIB PLDI'19 Semantics

• Matching mu-Logic

  Xiaohong Chen and Grigore Rosu
  LICS'19 ACM/IEEE, pp 1-13, June 2019
  PDF BIB LICS'19 Matching Logic

• Matching mu-Logic: Foundation of K Framework

  Xiaohong Chen and Grigore Rosu
  CALCO'19 Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik, Volume 139, pp 1-4, June 2019
  PDF BIB CALCO'19 Matching Logic

• Techniques for Evolution-Aware Runtime Verification

  Owolabi Legunsen and Yi Zhang and Milica Hadzi-Tanovic and Grigore Rosu and Darko Marinov
  ICST 2019 IEEE, pp 300-311, April 2019
  PDF BIB ICST 2019 JavaMOP

• Matching mu-Logic

  Xiaohong Chen and Grigore Rosu
  Technical Report January 2019 http://hdl.handle.net/2142/102281
  PDF BIB Matching Logic

• SETSS'19 Lecture Notes on K

  Xiaohong Chen and Grigore Rosu
  SETSS'19 Springer, 2019
  PDF BIB K

2018

• 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, November 2018
  PDF BIB ESEC/FSE'18 Formally Verified Smart Contracts

• A Language-Independent Program Verification Framework

  Xiaohong Chen and Grigore Rosu
  ISoLA'18 Springer, pp 92-102, November 2018
  PDF BIB ISoLA'18

• A Language-Independent Approach to Smart Contract Verification

  Xiaohong Chen and Daejun Park and Grigore Rosu
  ISoLA'18 Springer, pp 405-413, November 2018
  PDF BIB ISoLA'18 Formally Verified Smart Contracts

• 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 July 2018 http://hdl.handle.net/2142/100320
  PDF BIB IELE

• Program Verification by Coinduction

  Brandon Moore and Lucas Pena and Grigore Rosu
  ESOP'18 Springer, pp 589-618, April 2018
  PDF BIB ESOP'18 Matching Logic

• P4K: A Formal Semantics of P4 and Applications

  Ali Kheradmand and Grigore Rosu
  Technical Report April 2018 https://arxiv.org/abs/1804.01468
  PDF BIB P4K

• 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'18 IEEE, pp 204-217, 2018
  PDF BIB CSF'18 KEVM

2017

• Matching logic

  Grigore Rosu
  LMCS Volume 13, pp 1-61, December 2017
  PDF BIB LMCS

• Open Problems and Challenges 2017

  Grigore Rosu
  Technical Report March 2017 http://hdl.handle.net/2142/95775
  PDF BIB Webpage

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

  Grigore Rosu
  Marktoberdorf'16 {IOS} Press, 2017
  PDF BIB K

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, Nov 2016
  PDF BIB OOPSLA'16 Matching Logic

• Finite-Trace Linear Temporal Logic: Coinductive Completeness

  Grigore Rosu
  RV'16 Springer, Volume 10012, pp 333-350, September 2016
  PDF BIB RV'16 Matching Logic

• 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, September 2016
  PDF BIB ASE 2016 JavaMOP

• 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 Springer, Volume 10012, pp 46-67, September 2016
  PDF BIB RV'16 RV Products

• RV-Match: Practical Semantics-Based Program Analysis

  Dwight Guth and Chris Hathhorn and Manasvi Saxena and Grigore Rosu
  CAV'16 Springer, Volume 9779, pp 447-453, July 2016
  PDF BIB CAV'16 RV-Match

• A Language-Independent Proof System for Full Program Equivalence

  Stefan Ciobaca and Dorel Lucanu and Vlad Rusu and Grigore Rosu
  J.FAOC Volume 28, pp 469-497, May 2016
  PDF BIB J.FAOC Matching Logic

• RV-ECU: Maximum Assurance In-Vehicle Safety Monitoring

  Philip Daian and Bhargava Manja and Shinichi Shiraishi and Akihito Iwai and Grigore Rosu
  SAE'16 Volume 2016-01-0126, pp 1-13, April 2016
  PDF BIB SAE'16 RV-ECU

• Open Problems and Challenges 2016

  Grigore Rosu
  Technical Report February 2016 http://hdl.handle.net/2142/88925
  PDF BIB Webpage

• 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, pp 98-120, Jan 2016
  PDF BIB J.LAMP

• Towards a Kool Future

  Dorel Lucanu and Traian Florin Serbanuta and Grigore Rosu
  Boer's Festschrift Springer, Volume 9660, pp 325-343, January 2016
  PDF BIB Boer's Festschrift K

2015

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

  Grigore Rosu
  Meseguer's Festschrift Springer, Volume 9200, pp 598-616, September 2015
  PDF BIB Meseguer's Festschrift K

• 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 Springer, Volume 9333, pp 342-357, September 2015
  PDF BIB RV'15 RV-Android

• Matching Logic --- Extended Abstract

  Grigore Rosu
  RTA'15 Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik, Volume 36, pp 5-21, July 2015
  PDF BIB RTA'15 Matching Logic

• KJS: A Complete Formal Semantics of JavaScript

  Daejun Park and Andrei Stefanescu and Grigore Rosu
  PLDI'15 ACM, pp 346-356, June 2015
  PDF BIB PLDI'15 Semantics

• Defining the Undefinedness of C

  Chris Hathhorn and Chucky Ellison and Grigore Rosu
  PLDI'15 ACM, pp 336-345, June 2015
  PDF BIB PLDI'15 C Semantics

• Evolution-Aware Monitoring-Oriented Programming

  Owolabi Legunsen and Darko Marinov and Grigore Rosu
  ICSE NIER'15 ACM, pp 615-618, May 2015
  PDF BIB ICSE NIER'15 JavaMOP

• GPredict: Generic Predictive Concurrency Analysis

  Jeff Huang and Qingzhou Luo and Grigore Rosu
  ICSE'15 ACM, pp 847-857, May 2015
  PDF BIB ICSE'15 jPredictor

• Term-Generic Logic

  Andrei Popescu and Grigore Rosu
  Journal of Theoretical Computer Science Volume 577, pp 1-24, April 2015
  PDF BIB Journal of Theoretical Computer Science

• Program Verification by Coinduction

  Brandon Moore and Grigore Rosu
  Technical Report February 2015 http://hdl.handle.net/2142/73177
  PDF BIB Matching Logic

• K-Java: A Complete Semantics of Java

  Denis Bogdanas and Grigore Rosu
  POPL'15 ACM, pp 445-456, January 2015
  PDF BIB POPL'15 K-Java

2014

• A Language-Independent Proof System for Mutual Program Equivalence

  Stefan Ciobaca and Dorel Lucanu and Vlad Rusu and Grigore Rosu
  ICFEM'14 Springer, Volume 8829, pp 75-90, November 2014
  PDF BIB ICFEM'14 Matching Logic

• 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 Springer, Volume 8734, pp 285-300, September 2014
  PDF BIB RV'14 JavaMOP

• Symbolic Analysis Tools for CSP

  Liyi Li and Elsa Gunter and William Mansky
  ICTAC'14 Springer International Publishing, pp 295-313, Sep 2014
  PDF BIB ICTAC'14 Holistic CSP

• 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 Springer International Publishing, Volume 8734, pp 247-254, September 2014
  PDF BIB RV'14 ROSRV

• All-Path Reachability Logic

  Andrei Stefanescu and Stefan Ciobaca and Radu Mereuta and Brandon Moore and Traian Florin Serbanuta and Grigore Rosu
  RTA'14 Springer, Volume 8560, pp 425-440, July 2014
  PDF BIB RTA'14 Matching Logic

• Converting Parallel Code from Low-Level Abstractions to Higher-Level Abstractions

  Semih Okur and Cansu Erdogan and Danny Dig
  ECOOP'14 Springer, pp 515-540, July 2014
  PDF BIB ECOOP'14 Taskifier

• K Overview and SIMPLE Case Study

  Grigore Rosu and Traian Florin Serbanuta
  K'11 Elsevier, Volume 304, pp 3-56, June 2014
  PDF BIB K'11 K

• 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 Elsevier, Volume 304, pp 57-80, June 2014
  PDF BIB K'11 K

• Maximal Sound Predictive Race Detection with Control Flow Abstraction

  Jeff Huang and Patrick Meredith and Grigore Rosu
  PLDI'14 ACM, pp 337-348, June 2014
  PDF BIB PLDI'14 jPredictor

• Abstract Semantics for K Module Composition

  Codruta Girlea and Grigore Rosu
  K'11 Elsevier, Volume 304, pp 127-149, June 2014
  PDF BIB K'11 K

• On the Complexity of Stream Equality

  Joerg Endrullis and Dimitri Hendriks and Rena Bakhshi and Grigore Rosu
  Journal of Functional Programming Volume 24, pp 166-217, May 2014
  PDF BIB Journal of Functional Programming CIRC

• Behavioral Rewrite Systems and Behavioral Productivity

  Grigore Rosu and Dorel Lucanu
  Futatsugi Festschrift 2014 Volume 8373, pp 296-314, April 2014
  PDF BIB Futatsugi Festschrift 2014 CIRC

• 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 Springer, Volume 8663, pp 97-112, April 2014
  PDF BIB WRLA'14 K

• Matching Logic: A Logic for Structural Reasoning

  Grigore Rosu
  Technical Report Jan 2014 http://hdl.handle.net/2142/47004
  PDF BIB Matching Logic

• Optimizing SYB is Easy!

  Michael D. Adams and Andrew Farmer and Jose Pedro Magalhaes
  PEPM'14 ACM, pp 71-82, January 2014
  PDF BIB PEPM'14 Optimizing SYB

2013

• The Rewriting Logic Semantics Project: A Progress Report

  Jose Meseguer and Grigore Rosu
  Information and Computation Volume 231, pp 38-69, oct 2013
  PDF BIB Information and Computation K

• Specifying Languages and Verifying Programs with K

  Grigore Rosu
  SYNASC'13 IEEE, pp 28-31, September 2013
  PDF BIB SYNASC'13 K

• EnforceMOP: A Runtime Property Enforcement System for Multithreaded Programs

  Qingzhou Luo and Grigore Rosu
  ISSTA'13 ACM, pp 156-166, July 2013
  PDF BIB ISSTA'13 EnforceMOP

• One-Path Reachability Logic

  Grigore Rosu and Andrei Stefanescu and Stefan Ciobaca and Brandon Moore
  LICS'13 IEEE, pp 358-367, June 2013
  PDF BIB LICS'13 Reachability Logic

• Natural Proofs for Structure, Data, and Separation

  Xiaokang Qiu and Pranav Garg and Andrei Stefanescu and Parthasarathy Madhusudan
  PLDI'13 ACM, pp 231-242, June 2013
  PDF BIB PLDI'13 Dryad

• Low-Level Program Verification using Matching Logic Reachability

  Dwight Guth and Andrei Stefanescu and Grigore Rosu
  LOLA'13 , pp ---, June 2013
  PDF BIB LOLA'13 Matching Logic

• Efficient Parametric Runtime Verification with Deterministic String Rewriting

  Patrick Meredith and Grigore Rosu
  ASE'13 IEEE/ACM, pp 70-80, May 2013
  PDF BIB ASE'13 MOP

2012

• On Safety Properties and Their Monitoring

  Grigore Rosu
  SACS Volume 22, pp 327-365, December 2012
  PDF BIB SACS MOP

• Checking Reachability using Matching Logic

  Grigore Rosu and Andrei Stefanescu
  OOPSLA'12 ACM, pp 555-574, Oct 2012
  PDF BIB OOPSLA'12 Matching Logic

• A Truly Concurrent Semantics for the K Framework Based on Graph Transformations

  Traian Florin Serbanuta and Grigore Rosu
  ICGT'12 Springer, Volume 7562, pp 294-310, September 2012
  PDF BIB ICGT'12 K

• Maximal Causal Models for Sequentially Consistent Systems

  Traian Florin Serbanuta and Feng Chen and Grigore Rosu
  RV'12 Springer, Volume 7687, pp 136-150, September 2012
  PDF BIB RV'12 JPredictor

• From Hoare Logic to Matching Logic Reachability

  Grigore Rosu and Andrei Stefanescu
  FM'12 Springer, Volume 7436, pp 387-402, Aug 2012
  PDF BIB FM'12 Matching Logic

• Efficient, Expressive, and Effective Runtime Verification

  Patrick O'Neil Meredith
  PhD Thesis August 2012
  PDF BIB MOP

• Executing Formal Semantics with the K Tool

  David Lazar and Andrei Arusoaie and Traian Florin Serbanuta and Chucky Ellison and Radu Mereuta and Dorel Lucanu and Grigore Rosu
  FM'12 Springer, Volume 7436, pp 267-271, August 2012
  PDF BIB FM'12 K

• Making Runtime Monitoring of Parametric Properties Practical

  Dongyun Jin
  PhD Thesis August 2012
  PDF BIB MOP

• Reachability Logic

  Grigore Rosu and Andrei Stefanescu and Stefan Ciobaca and Brandon Moore
  Technical Report Jul 2012 http://hdl.handle.net/2142/32952
  PDF BIB Reachability Logic

• Towards a Unified Theory of Operational and Axiomatic Semantics

  Grigore Rosu and Andrei Stefanescu
  ICALP'12 Springer, Volume 7392, pp 351-363, Jul 2012
  PDF BIB ICALP'12 Matching Logic

• A Formal Semantics of C with Applications

  Chucky Ellison
  PhD Thesis July 2012
  PDF BIB K

• Test-Case Reduction for C Compiler Bugs

  John Regehr and Yang Chen and Pascal Cuoq and Eric Eide and Chucky Ellison and Xuejun Yang
  PLDI'12 ACM, pp 335-346, June 2012
  PDF BIB PLDI'12 C-Reduce

• JavaMOP: Efficient Parametric Runtime Monitoring Framework

  Dongyun Jin and Patrick O'Neil Meredith and Choonghwan Lee and Grigore Rosu
  ICSE'12 IEEE, pp 1427-1430, June 2012
  PDF BIB ICSE'12 MOP

• Security-Policy Monitoring and Enforcement with JavaMOP

  Soha Hussein and Patrick Meredith and Grigore Rosu
  PLAS'12 ACM, pp 3:1-3:11, June 2012
  PDF BIB PLAS'12 MOP

• Scalable Parametric Runtime Monitoring

  Dongyun Jin and Patrick O'Neil Meredith and Grigore Rosu
  Technical Report April 2012 http://hdl.handle.net/2142/30757
  PDF BIB MOP

• Defining the Undefinedness of C

  Chucky Ellison and Grigore Rosu
  Technical Report April 2012 http://hdl.handle.net/2142/30780
  PDF BIB K

• K Framework Distilled

  Dorel Lucanu and Traian Florin Serbanuta and Grigore Rosu
  WRLA'12 Springer, Volume 7571, pp 31-53, March 2012
  PDF BIB WRLA'12 K

• Towards Categorizing and Formalizing the JDK API

  Choonghwan Lee and Dongyun Jin and Patrick O'Neil Meredith and Grigore Rosu
  Technical Report March 2012 http://hdl.handle.net/2142/30006
  PDF BIB Java API

• Making Maude Definitions more Interactive

  Andrei Arusoaie and Traian Florin Serbanuta and Chucky Ellison and Grigore Rosu
  WRLA'12 Springer, Volume 7571, pp 83-98, March 2012
  PDF BIB WRLA'12 K

• Semantics and Algorithms for Parametric Monitoring

  Grigore Rosu and Feng Chen
  J.LMCS Volume 8, pp 1-47, Feb 2012
  PDF BIB J.LMCS MOP

• Recursive Proofs for Inductive Tree Data-Structures

  Parthasarathy Madhusudan and Xiaokang Qiu and Andrei Stefanescu
  POPL'12 ACM, pp 123-136, Jan 2012
  PDF BIB POPL'12 Dryad

• An Executable Formal Semantics of C with Applications

  Chucky Ellison and Grigore Rosu
  POPL'12 ACM, pp 533-544, January 2012
  PDF BIB POPL'12 Semantics

2011

• Maximal Causal Models for Sequentially Consistent Systems

  Traian Florin Serbanuta and Feng Chen and Grigore Rosu
  Technical Report October 2011 http://hdl.handle.net/2142/27708
  PDF BIB JPredictor

• 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, September 2011
  PDF BIB FSE'11

• MatchC: A Matching Logic Reachability Verifier Using the K Framework

  Andrei Stefanescu
  K'11 Springer, Volume 304, August 2011
  PDF BIB Matching Logic

• The Rewriting Logic Semantics Project: A Progress Report

  Jose Meseguer and Grigore Rosu
  FCT'11 Springer, Volume 6914, pp 1-37, August 2011
  PDF BIB FCT'11 K

• An Executable Formal Semantics of C with Applications

  Chucky Ellison and Grigore Rosu
  Technical Report July 2011 http://hdl.handle.net/2142/25816
  PDF BIB C Semantics

• Towards Semantics-Based WCET Analysis

  Mihail Asavoae and Dorel Lucanu and Grigore Rosu
  WCET'11 Austrian Computer Society, Volume , pp , July 2011
  PDF BIB WCET'11 Matching Logic

• 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 Springer, Volume 14, pp 249-289, June 2011
  PDF BIB J.STTT MOP

• 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, June 2011
  PDF BIB PLDI'11 MOP

• Matching Logic: A New Program Verification Approach (NIER Track)

  Grigore Rosu and Andrei Stefanescu
  ICSE'11 ACM, pp 868-871, May 2011
  PDF BIB ICSE'11 Matching Logic

• Mining Parametric Specifications

  Choonghwan Lee and Feng Chen and Grigore Rosu
  ICSE'11 ACM, pp 591-600, May 2011
  PDF BIB ICSE'11 JMiner

2010

• A Rewriting Approach to Concurrent Programming Language Design and Semantics

  Traian Florin Serbanuta
  PhD Thesis December 2010
  PDF BIB K

• Matching Logic: A New Program Verification Approach

  Grigore Rosu and Andrei Stefanescu
  UV'10 Nov 2010
  PDF BIB UV'10 Matching Logic

• Runtime Verification with the RV System

  Patrick Meredith and Grigore Rosu
  RV'10 Springer, pp 136-152, November 2010
  PDF BIB RV'10 RV

• Automating Coinduction with Case Analysis

  Eugen-Ioan Goriac and Dorel Lucanu and Grigore Rosu
  ICFEM'10 Springer, pp 220-236, November 2010
  PDF BIB ICFEM'10 Circ

• A Formal Semantics of C with Applications

  Chucky Ellison and Grigore Rosu
  Technical Report November 2010 http://hdl.handle.net/2142/17414
  PDF BIB C Semantics

• Maximal Causal Models for Sequentially Consistent Multithreaded Systems

  Traian Florin Serbanuta and Feng Chen and Grigore Rosu
  Technical Report September 2010 http://hdl.handle.net/2142/17336
  PDF BIB JPredictor

• Matching Logic: An Alternative to Hoare/Floyd Logic

  Grigore Rosu and Chucky Ellison and Wolfram Schulte
  AMAST'10 Springer, pp 142-162, June 2010
  PDF BIB AMAST'10 Matching Logic

• K-Maude: A Rewriting Based Tool for Semantics of Programming Languages

  Traian Florin Serbanuta and Grigore Rosu
  WRLA'10 Springer, pp 104-122, March 2010
  PDF BIB WRLA'10 K

2009

• Matching Logic --- Extended Report

  Grigore Rosu and Wolfram Schulte
  Technical Report January 2009 http://hdl.handle.net/2142/10790
  PDF BIB Matching Logic

2005

• Monitoring Algorithms for Metric Temporal Logic

  Prasanna Thati and Grigore Rosu
  RV'05 Elsevier, Volume 113, pp 145-162, June 2005
  PDF BIB RV'05 MOP

• Rewriting-Based Techniques for Runtime Verification

  Grigore Rosu and Klaus Havelund
  J.ASE Volume 12, pp 151-197, 2005
  PDF BIB J.ASE MOP

2004

• Composing Hidden Information Modules over Inclusive Institutions

  Joseph Goguen and Grigore Rosu
  Dahl's Festschrift Springer Berlin Heidelberg, Volume 2635, pp 96-123, September 2004
  PDF BIB Dahl's Festschrift

2003

• Generating Optimal Linear Temporal Logic Monitors by Coinduction

  Koushik Sen and Grigore Rosu and Gul Agha
  ASIAN'03 Springer-Verlag, Volume 2896, pp 260-275, December 2003
  PDF BIB ASIAN'03 MOP

• CS322 - Programming Language Design: Lecture Notes

  Grigore Rosu
  Technical Report December 2003 http://hdl.handle.net/2142/11385
  PDF BIB Matching Logic

• Certifying Measurement Unit Safety Policy

  Grigore Rosu and Feng Chen
  ASE'03 IEEE, pp 304-309, October 2003
  PDF BIB ASE'03 MOP

• Certifying and Synthesizing Membership Equational Proofs

  Grigore Rosu and Steven Eker and Patrick Lincoln and Jose Meseguer
  FME'03 Springer-Verlag, Volume 2805, pp 359-380, September 2003
  PDF BIB FME'03 Maude

• Generating Optimal Monitors for Extended Regular Expressions

  Koushik Sen and Grigore Rosu
  RV'03 Elsevier, Volume 89(2), pp 226-245, June 2003
  PDF BIB RV'03 MOP

• Testing Extended Regular Language Membership Incrementally by Rewriting

  Grigore Rosu and Mahesh Viswanathan
  RTA'03 Springer-Verlag, Volume 2706, pp 499-514, June 2003
  PDF BIB RTA'03 MOP

• Rule-Based Analysis of Dimensional Safety

  Feng Chen and Grigore Rosu and Ram prasad Venkatesan
  RTA'03 Springer-Verlag, Volume 2706, pp 197-207, June 2003
  PDF BIB RTA'03 MOP

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

  Feng Chen and Grigore Rosu
  RV'03 Elsevier, Volume 89(2), pp 108-127, June 2003
  PDF BIB RV'03 MOP

• Inductive Behavioral Proofs by Unhiding

  Grigore Rosu
  CMCS'03 Volume 82, pp 285-302, April 2003
  PDF BIB CMCS'03 Logic

2002

• Synthesizing Monitors for Safety Properties

  Klaus Havelund and Grigore Rosu
  TACAS'02 Springer, Volume 2280, pp 342-356, April 2002
  PDF BIB TACAS'02 MOP

2001

• Interpreting Abstract Interpretations in Membership Equational Logic

  Bernd Fischer and Grigore Rosu
  RULE'01 Elsevier, Volume 59(4), pp 271-285, June 2001
  PDF BIB Maude

• Certifying Domain-Specific Policies

  Michael Lowry and Thomas Pressburger and Grigore Rosu
  ASE'01 IEEE, pp 81-90, May 2001
  PDF BIB ASE'01 AutoFilter

• Monitoring Programs using Rewriting

  Klaus Havelund and Grigore Rosu
  ASE'01 IEEE, pp 135-143, May 2001
  PDF BIB ASE'01 MOP

• Synthesizing Dynamic Programming Algorithms from Linear Temporal Logic Formulae

  Grigore Rosu and Klaus Havelund
  Technical Report January 2001 https://ti.arc.nasa.gov/m/pub-archive/archive/0220.pdf
  PDF BIB

2000

• Abstract Semantics for Module Composition

  Grigore Rosu
  Technical Report May 2000 http://roger.ucsd.edu/record=b7304233~S9
  PDF BIB