Grigore Rosu’s Publications

2020

• A General Approach to Define Binders Using Matching Logic
  Chen, Xiaohong and Roşu, Grigore.
  ICFP’20 ACM/IEEE, pp 1-32.
  2020
  PDF BIB
• Towards A Unified Proof Framework for Automated Fixpoint Reasoning Using Matching Logic
  Chen, Xiaohong and Trinh, Minh-Thai and Rodrigues, Nishant and Peña, Lucas and Roşu, Grigore.
  2020
  PDF BIB
• Connecting Constrained Constructor Patterns and Matching Logic
  Chen, Xiaohong and Lucanu, Dorel and Roşu, Grigore.
  WRLA’20 , pp .
  2020
  PDF BIB
• Formal Semantics of Hybrid Automata
  Saxena, Manasvi and Rodrigues, Nishant and Chen, Xiaohong and Roşu, Grigore.
  2020
  PDF BIB
• Initial algebra semantics in matching logic
  Chen, Xiaohong and Lucanu, Dorel and Roşu, Grigore.
  2020
  PDF BIB
• Towards A Unified Proof Framework for Automated Fixpoint Reasoning Using Matching Logic
  Chen, Xiaohong and Trinh, Minh-Thai and Rodrigues, Nishant and Peña, Lucas and Roşu, Grigore.
  OOPSLA’20 ACM/IEEE, pp 1-29.
  2020
  PDF BIB
• A General Approach to Define Binders Using Matching Logic
  Chen, Xiaohong and Roşu, Grigore.
  2020
  PDF BIB
• Matching Logic Explained
  Chen, Xiaohong and Lucanu, Dorel and Roşu, Grigore.
  2020
  PDF BIB

2019

• SETSS’19 Lecture Notes on K
  Chen, Xiaohong and Rosu, Grigore.
  SETSS’19 Springer, pp .
  2019
  PDF BIB
• Techniques for Evolution-Aware Runtime Verification
  Legunsen, Owolabi and Zhang, Yi and Hadzi-Tanovic, Milica and Roşu, Grigore and Marinov, Darko.
  ICST 2019 IEEE, pp 300-311.
  2019
  PDF BIB
• A Complete Formal Semantics of x86-64 User-Level Instruction Set Architecture
  Dasgupta, Sandeep and Park, Daejun and Kasampalis, Theodoros and Adve, Vikram S. and Roşu, Grigore.
  PLDI’19 ACM, pp 1133-1148.
  2019
  PDF BIB
• Matching mu-Logic
  Chen, Xiaohong and Roşu, Grigore.
  2019
  PDF BIB
• Applicative Matching Logic: Semantics of K
  Chen, Xiaohong and Roşu, Grigore.
  2019
  PDF BIB
• Matching mu-Logic
  Chen, Xiaohong and Roşu, Grigore.
  LICS’19 ACM/IEEE, pp 1-13.
  2019
  PDF BIB
• 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.
  2019
  PDF BIB
• Matching mu-Logic: Foundation of K Framework
  Chen, Xiaohong and Roşu, Grigore.
  CALCO’19 Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik, pp 1-4.
  2019
  PDF BIB

2018

• KEVM: A Complete Semantics of the Ethereum Virtual Machine
  Hildenbrandt, Everett and Saxena, Manasvi and Zhu, Xiaoran and Rodrigues, Nishant and Daian, Philip and Guth, Dwight and Moore, Brandon and Zhang, Yi and Park, Daejun and Ştefănescu, Andrei and Roşu, Grigore.
  CSF’18 IEEE, pp 204-217.
  2018
  PDF BIB
• P4K: A Formal Semantics of P4 and Applications
  Kheradmand, Ali and Roşu, Grigore.
  2018
  PDF BIB
• Program Verification by Coinduction
  Moore, Brandon and Peña, Lucas and Roşu, Grigore.
  ESOP’18 Springer, pp 589-618.
  2018
  PDF BIB
• A Formal Verification Tool for Ethereum VM Bytecode
  Park, Daejun and Zhang, Yi and Saxena, Manasvi and Daian, Philip and Roşu, Grigore.
  ESEC/FSE’18 ACM, pp 912-915.
  2018
  PDF BIB
• A Language-Independent Approach to Smart Contract Verification
  Chen, Xiaohong and Park, Daejun and Roşu, Grigore.
  ISoLA’18 Springer, pp 405-413.
  2018
  PDF BIB
• IELE: An Intermediate-Level Blockchain Language Designed and Implemented Using Formal Semantics
  Kasampalis, Theodoros and Guth, Dwight and Moore, Brandon and Serbanuta, Traian and Serbanuta, Virgil and Filaretti, Daniele and Rosu, Grigore and Johnson, Ralph.
  2018
  PDF BIB
• A Language-Independent Program Verification Framework
  Chen, Xiaohong and Roşu, Grigore.
  ISoLA’18 Springer, pp 92-102.
  2018
  PDF BIB

2017

• Matching logic
  Roşu, Grigore.
  2017
  PDF BIB
• K - A Semantic Framework for Programming Languages and Formal Analysis Tools
  Rosu, Grigore.
  Marktoberdorf’16 IOS Press, pp .
  2017
  PDF BIB
• Open Problems and Challenges 2017
  Rosu, Grigore.
  2017
  PDF BIB

2016

• A Language-Independent Proof System for Full Program Equivalence
  Ciobaca, Stefan and Lucanu, Dorel and Rusu, Vlad and Rosu, Grigore.
  2016
  PDF BIB
• RV-Match: Practical Semantics-Based Program Analysis
  Guth, Dwight and Hathhorn, Chris and Saxena, Manasvi and Rosu, Grigore.
  CAV’16 Springer, pp 447-453.
  2016
  PDF BIB
• RV-ECU: Maximum Assurance In-Vehicle Safety Monitoring
  Daian, Philip and Manja, Bhargava and Shiraishi, Shinichi and Iwai, Akihito and Rosu, Grigore.
  SAE’16 , pp 1-13.
  2016
  PDF BIB
• Runtime Verification at Work: A Tutorial
  Daian, Philip and Guth, Dwight and Hathhorn, Chris and Li, Yilong and Pek, Edgar and Saxena, Manasvi and Serbanuta, Traian Florin and Rosu, Grigore.
  RV’16 Springer, pp 46-67.
  2016
  PDF BIB
• Towards a Kool Future
  Lucanu, Dorel and Şerbănuţă, Traian Florin and Roşu, Grigore.
  Boer’s Festschrift Springer, pp 325-343.
  2016
  PDF BIB
• How Good are the Specs? A Study of the Bug-Finding Effectiveness of Existing Java API Specifications
  Legunsen, Owolabi and Hassan, Wajih Ul and Xu, Xinyue and Roşu, Grigore and Marinov, Darko.
  ASE 2016 IEEE/ACM, pp 602-613.
  2016
  PDF BIB
• Language Definitions as Rewrite Theories
  Rusu, Vlad and Lucanu, Dorel and Şerbănuţă, Traian-Florin and Arusoaie, Andrei and Ştefănescu, Andrei and Roşu, Grigore.
  2016
  PDF BIB
• Semantics-Based Program Verifiers for All Languages
  Ştefănescu, Andrei and Park, Daejun and Yuwen, Shijiao and Li, Yilong and Roşu, Grigore.
  OOPSLA’16 ACM, pp 74-91.
  2016
  PDF BIB
• Open Problems and Challenges 2016
  Rosu, Grigore.
  2016
  PDF BIB
• Finite-Trace Linear Temporal Logic: Coinductive Completeness
  Roşu, Grigore.
  RV’16 Springer, pp 333-350.
  2016
  PDF BIB

2015

• Program Verification by Coinduction
  Moore, Brandon and Roşu, Grigore.
  2015
  PDF BIB
• From Rewriting Logic, to Programming Language Semantics, to Program Verification
  Roşu, Grigore.
  Meseguer’s Festschrift Springer, pp 598-616.
  2015
  PDF BIB
• GPredict: Generic Predictive Concurrency Analysis
  Huang, Jeff and Luo, Qingzhou and Rosu, Grigore.
  ICSE’15 ACM, pp 847-857.
  2015
  PDF BIB
• Term-Generic Logic
  Popescu, Andrei and Roşu, Grigore.
  2015
  PDF BIB
• K-Java: A Complete Semantics of Java
  Bogdănaş, Denis and Roşu, Grigore.
  POPL’15 ACM, pp 445-456.
  2015
  PDF BIB
• Evolution-Aware Monitoring-Oriented Programming
  Legunsen, Owolabi and Marinov, Darko and Roşu, Grigore.
  ICSE NIER’15 ACM, pp 615-618.
  2015
  PDF BIB
• Defining the Undefinedness of C
  Hathhorn, Chris and Ellison, Chucky and Roşu, Grigore.
  PLDI’15 ACM, pp 336-345.
  2015
  PDF BIB
• RV-Android: Efficient Parametric Android Runtime Verification, a Brief Tutorial
  Daian, Philip and Falcone, Yliès and Meredith, Patrick O’Neil and Serbanuta, Traian-Florin and Shiraishi, Shinichi and Iwai, Akihito and Rosu, Grigore.
  RV’15 Springer, pp 342-357.
  2015
  PDF BIB
• KJS: A Complete Formal Semantics of JavaScript
  Park, Daejun and Ştefănescu, Andrei and Roşu, Grigore.
  PLDI’15 ACM, pp 346-356.
  2015
  PDF BIB
• Matching Logic — Extended Abstract
  Roşu, Grigore.
  RTA’15 Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik, pp 5-21.
  2015
  PDF BIB

2014

• A Language-Independent Proof System for Mutual Program Equivalence
  Ciobaca, Stefan and Lucanu, Dorel and Rusu, Vlad and Rosu, Grigore.
  ICFEM’14 Springer, pp 75-90.
  2014
  PDF BIB
• Behavioral Rewrite Systems and Behavioral Productivity
  Rosu, Grigore and Lucanu, Dorel.
  Futatsugi Festschrift 2014 , pp 296-314.
  2014
  PDF BIB
• K Overview and SIMPLE Case Study
  Rosu, Grigore and Serbanuta, Traian Florin.
  K’11 Elsevier, pp 3-56.
  2014
  PDF BIB
• Maximal Sound Predictive Race Detection with Control Flow Abstraction
  Huang, Jeff and Meredith, Patrick and Rosu, Grigore.
  PLDI’14 ACM, pp 337-348.
  2014
  PDF BIB
• RV-Monitor: Efficient Parametric Runtime Verification with Simultaneous Properties
  Luo, Qingzhou and Zhang, Yi and Lee, Choonghwan and Jin, Dongyun and Meredith, Patrick O’Neil and Serbanuta, Traian Florin and Rosu, Grigore.
  RV’14 Springer, pp 285-300.
  2014
  PDF BIB
• Abstract Semantics for K Module Composition
  Girlea, Codruta and Rosu, Grigore.
  K’11 Elsevier, pp 127-149.
  2014
  PDF BIB
• Language Definitions as Rewrite Theories
  Arusoaie, Andrei and Lucanu, Dorel and Rusu, Vald and Şerbănuţă, Traian Florin and Ştefănescu, Andrei and Roşu, Grigore.
  WRLA’14 Springer, pp 97-112.
  2014
  PDF BIB
• ROSRV: Runtime Verification for Robots
  Huang, Jeff and Erdogan, Cansu and Zhang, Yi and Moore, Brandon and Luo, Qingzhou and Sundaresan, Aravind and Rosu, Grigore.
  RV’14 Springer International Publishing, pp 247-254.
  2014
  PDF BIB
• All-Path Reachability Logic
  Ştefănescu, Andrei and Ştefan Ciobâcă and Mereuţă, Radu and Moore, Brandon M. and Şerbănuţă, Traian Florin and Roşu, Grigore.
  RTA’14 Springer, pp 425-440.
  2014
  PDF BIB
• On the Complexity of Stream Equality
  Endrullis, Jörg and Hendriks, Dimitri and Bakhshi, Rena and Roşu, Grigore.
  2014
  PDF BIB
• Matching Logic: A Logic for Structural Reasoning
  Roşu, Grigore.
  2014
  PDF BIB
• The K Primer (version 3.3)
  Serbanuta, Traian Florin and Arusoaie, Andrei and Lazar, David and Ellison, Chucky and Lucanu, Dorel and Rosu, Grigore.
  K’11 Elsevier, pp 57-80.
  2014
  PDF BIB

2013

• Efficient Parametric Runtime Verification with Deterministic String Rewriting
  Meredith, Patrick and Rosu, Grigore.
  ASE’13 IEEE/ACM, pp 70-80.
  2013
  PDF BIB
• One-Path Reachability Logic
  Roşu, Grigore and Ştefănescu, Andrei and Ştefan Ciobâcă and Moore, Brandon M..
  LICS’13 IEEE, pp 358-367.
  2013
  PDF BIB
• Specifying Languages and Verifying Programs with K
  Rosu, Grigore.
  SYNASC’13 IEEE, pp 28-31.
  2013
  PDF BIB
• EnforceMOP: A Runtime Property Enforcement System for Multithreaded Programs
  Luo, Qingzhou and Rosu, Grigore.
  ISSTA’13 ACM, pp 156-166.
  2013
  PDF BIB
• Low-Level Program Verification using Matching Logic Reachability
  Guth, Dwight and Ştefănescu, Andrei and Roşu, Grigore.
  LOLA’13 , pp —.
  2013
  PDF BIB
• The Rewriting Logic Semantics Project: A Progress Report
  Meseguer, José and Roşu, Grigore.
  2013
  PDF BIB

2012

• Making Maude Definitions more Interactive
  Arusoaie, Andrei and Şerbănuţă, Traian Florin and Ellison, Chucky and Roşu, Grigore.
  WRLA’12 Springer, pp 83-98.
  2012
  PDF BIB
• Maximal Causal Models for Sequentially Consistent Systems
  Serbanuta, Traian Florin and Chen, Feng and Rosu, Grigore.
  RV’12 Springer, pp 136-150.
  2012
  PDF BIB
• An Executable Formal Semantics of C with Applications
  Ellison, Chucky and Rosu, Grigore.
  POPL’12 ACM, pp 533-544.
  2012
  PDF BIB
• Executing Formal Semantics with the K Tool
  Lazar, David and Arusoaie, Andrei and Serbanuta, Traian Florin and Ellison, Chucky and Mereuta, Radu and Lucanu, Dorel and Roşu, Grigore.
  FM’12 Springer, pp 267-271.
  2012
  PDF BIB
• On Safety Properties and Their Monitoring
  Roşu, Grigore.
  2012
  PDF BIB
• Towards Categorizing and Formalizing the JDK API
  Lee, Choonghwan and Jin, Dongyun and Meredith, Patrick O’Neil and Roşu, Grigore.
  2012
  PDF BIB
• Scalable Parametric Runtime Monitoring
  Jin, Dongyun and Meredith, Patrick O’Neil and Roşu, Grigore.
  2012
  PDF BIB
• JavaMOP: Efficient Parametric Runtime Monitoring Framework
  Jin, Dongyun and Meredith, Patrick O’Neil and Lee, Choonghwan and Roşu, Grigore.
  ICSE’12 IEEE, pp 1427-1430.
  2012
  PDF BIB
• K Framework Distilled
  Lucanu, Dorel and Şerbănuţă, Traian Florin and Roşu, Grigore.
  WRLA’12 Springer, pp 31-53.
  2012
  PDF BIB
• Semantics and Algorithms for Parametric Monitoring
  Roşu, Grigore and Chen, Feng.
  2012
  PDF BIB
• A Truly Concurrent Semantics for the K Framework Based on Graph Transformations
  Serbanuta, Traian Florin and Rosu, Grigore.
  ICGT’12 Springer, pp 294-310.
  2012
  PDF BIB
• Towards a Unified Theory of Operational and Axiomatic Semantics
  Roşu, Grigore and Ştefănescu, Andrei.
  ICALP’12 Springer, pp 351-363.
  2012
  PDF BIB
• Defining the Undefinedness of C
  Ellison, Chucky and Roşu, Grigore.
  2012
  PDF BIB
• From Hoare Logic to Matching Logic Reachability
  Roşu, Grigore and Ştefănescu, Andrei.
  FM’12 Springer, pp 387-402.
  2012
  PDF BIB
• Reachability Logic
  Roşu, Grigore and Ştefănescu, Andrei and Ştefan Ciobâcă and Moore, Brandon M..
  2012
  PDF BIB
• Checking Reachability using Matching Logic
  Roşu, Grigore and Ştefănescu, Andrei.
  OOPSLA’12 ACM, pp 555-574.
  2012
  PDF BIB

2011

• Maximal Causal Models for Sequentially Consistent Systems
  Şerbănuţă, Traian Florin and Chen, Feng and Roşu, Grigore.
  2011
  PDF BIB
• An Executable Formal Semantics of C with Applications
  Ellison, Chucky and Roşu, Grigore.
  2011
  PDF BIB
• Towards Semantics-Based WCET Analysis
  Asavoae, Mihail and Lucanu, Dorel and Rosu, Grigore.
  WCET’11 Austrian Computer Society, pp .
  2011
  PDF BIB
• Mining Parametric Specifications
  Lee, Choonghwan and Chen, Feng and Roşu, Grigore.
  ICSE’11 ACM, pp 591-600.
  2011
  PDF BIB
• Matching Logic: A New Program Verification Approach (NIER Track)
  Roşu, Grigore and Ştefănescu, Andrei.
  ICSE’11 ACM, pp 868-871.
  2011
  PDF BIB
• An Overview of the MOP Runtime Verification Framework
  Meredith, Patrick O’Neil and Jin, Dongyun and Griffith, Dennis and Chen, Feng and Roşu, Grigore.
  2011
  PDF BIB
• Improved Multithreaded Unit Testing
  Jagannath, Vilas and Gligoric, Milos and Jin, Dongyun and Luo, Qingzhou and Roşu, Grigore and Marinov, Darko.
  FSE’11 ACM, pp 223-233.
  2011
  PDF BIB
• The Rewriting Logic Semantics Project: A Progress Report
  Meseguer, José and Roşu, Grigore.
  FCT’11 Springer, pp 1-37.
  2011
  PDF BIB
• Garbage Collection for Monitoring Parametric Properties
  Jin, Dongyun and Meredith, Patrick O’Neil and Griffith, Dennis and Roşu, Grigore.
  PLDI’11 ACM, pp 415-424.
  2011
  PDF BIB

2010

• A Formal Semantics of C with Applications
  Ellison, Chucky and Roşu, Grigore.
  2010
  PDF BIB
• Runtime Verification with the RV System
  Meredith, Patrick and Roşu, Grigore.
  RV’10 Springer, pp 136-152.
  2010
  PDF BIB
• Maximal Causal Models for Sequentially Consistent Multithreaded Systems
  Şerbănuţă, Traian Florin and Chen, Feng and Roşu, Grigore.
  2010
  PDF BIB
• Automating Coinduction with Case Analysis
  Goriac, Eugen-Ioan and Lucanu, Dorel and Roşu, Grigore.
  ICFEM’10 Springer, pp 220-236.
  2010
  PDF BIB
• Matching Logic: A New Program Verification Approach
  Roşu, Grigore and Ştefănescu, Andrei.
  UV’10 , pp .
  2010
  PDF BIB
• Matching Logic: An Alternative to Hoare/Floyd Logic
  Roşu, Grigore and Ellison, Chucky and Schulte, Wolfram.
  AMAST’10 Springer, pp 142-162.
  2010
  PDF BIB
• K-Maude: A Rewriting Based Tool for Semantics of Programming Languages
  Şerbanuţă, Traian Florin and Roşu, Grigore.
  WRLA’10 Springer, pp 104-122.
  2010
  PDF BIB

2009

• Matching Logic — Extended Report
  Rosu, Grigore and Schulte, Wolfram.
  2009
  PDF BIB

2005

• Rewriting-Based Techniques for Runtime Verification
  Rosu, Grigore and Havelund, Klaus.
  2005
  PDF BIB
• Monitoring Algorithms for Metric Temporal Logic
  Thati, Prasanna and Rosu, Grigore.
  RV’05 Elsevier, pp 145-162.
  2005
  PDF BIB

2004

• Composing Hidden Information Modules over Inclusive Institutions
  Goguen, Joseph and Rosu, Grigore.
  Dahl’s Festschrift Springer Berlin Heidelberg, pp 96-123.
  2004
  PDF BIB

2003

• CS322 - Programming Language Design: Lecture Notes
  Roşu, Grigore.
  2003
  PDF BIB
• Generating Optimal Monitors for Extended Regular Expressions
  Sen, Koushik and Rosu, Grigore.
  RV’03 Elsevier, pp 226-245.
  2003
  PDF BIB
• Towards Monitoring-Oriented Programming: A Paradigm Combining Specification and Implementation
  Chen, Feng and Roşu, Grigore.
  RV’03 Elsevier, pp 108-127.
  2003
  PDF BIB
• Certifying and Synthesizing Membership Equational Proofs
  Rosu, Grigore and Eker, Steven and Lincoln, Patrick and Meseguer, Jose.
  FME’03 Springer-Verlag, pp 359-380.
  2003
  PDF BIB
• Testing Extended Regular Language Membership Incrementally by Rewriting
  Rosu, Grigore and Viswanathan, Mahesh.
  RTA’03 Springer-Verlag, pp 499-514.
  2003
  PDF BIB
• Rule-Based Analysis of Dimensional Safety
  Chen, Feng and Roşu, Grigore and prasad Venkatesan, Ram.
  RTA’03 Springer-Verlag, pp 197-207.
  2003
  PDF BIB
• Generating Optimal Linear Temporal Logic Monitors by Coinduction
  Sen, Koushik and Rosu, Grigore and Agha, Gul.
  ASIAN’03 Springer-Verlag, pp 260-275.
  2003
  PDF BIB
• Inductive Behavioral Proofs by Unhiding
  Rosu, Grigore.
  2003
  PDF BIB
• Certifying Measurement Unit Safety Policy
  Roşu, Grigore and Chen, Feng.
  ASE’03 IEEE, pp 304-309.
  2003
  PDF BIB

2002

• Synthesizing Monitors for Safety Properties
  Havelund, Klaus and Rosu, Grigore.
  TACAS’02 Springer, pp 342-356.
  2002
  PDF BIB

2001

• Certifying Domain-Specific Policies
  Lowry, Michael and Pressburger, Thomas and Rosu, Grigore.
  ASE’01 IEEE, pp 81-90.
  2001
  PDF BIB
• Monitoring Programs using Rewriting
  Havelund, Klaus and Rosu, Grigore.
  ASE’01 IEEE, pp 135-143.
  2001
  PDF BIB
• Interpreting Abstract Interpretations in Membership Equational Logic
  Fischer, Bernd and Rosu, Grigore.
  RULE’01 Elsevier, pp 271-285.
  2001
  PDF BIB
• Synthesizing Dynamic Programming Algorithms from Linear Temporal Logic Formulae
  Rosu, Grigore and Havelund, Klaus.
  2001
  PDF BIB

2000

• Abstract Semantics for Module Composition
  Rosu, Grigore.
  2000
  PDF BIB