The Institution of Order-Sorted Equational Logic. - Grigore Rosu (Bull. EATCS, 1994)

Distributed Cooperative Formal Methods Tools. - Joseph A. Goguen; Kai Lin; Akira Mori; Grigore Rosu; Akiyoshi Sato (ASE, 1997)

Weak Inclusion Systems. - Virgil Emil Cazanescu; Grigore Rosu (Math. Struct. Comput. Sci., 1997)

Hidden Congruent Deduction. - Grigore Rosu; Joseph A. Goguen (FTP (LNCS Selection), 1998)

A Birkhoff-like Axiomatizability Result for Hidden Algebra and Coalgebra. - Grigore Rosu (CMCS, 1998)

Hiding More of Hidden Algebra. - Joseph A. Goguen; Grigore Rosu (World Congress on Formal Methods, 1999)

A protocol for distributed cooperative work. - Joseph A. Goguen; Grigore Rosu (WDS@FCT, 1999)

Kan Extensions of Institutions. - Grigore Rosu (J. Univers. Comput. Sci., 1999)

Circular Coinductive Rewriting. - Joseph A. Goguen; Kai Lin; Grigore Rosu (ASE, 2000)

Incompleteness of Behavioral Logics. - Samuel R. Buss; Grigore Rosu (CMCS, 2000)

Behavioral and Coinductive Rewriting. - Joseph A. Goguen; Kai Lin; Grigore Rosu (WRLA, 2000)

Weak Inclusion Systems: Part Two. - Virgil Emil Cazanescu; Grigore Rosu (J. Univers. Comput. Sci., 2000)

On Equational Craig Interpolation. - Grigore Rosu; Joseph A. Goguen (J. Univers. Comput. Sci., 2000)

Complete Categorical Equational Deduction. - Grigore Rosu (CSL, 2001)

Monitoring Programs Using Rewriting. - Klaus Havelund; Grigore Rosu (ASE, 2001)

Certifying Domain-Specific Policies. - Michael R. Lowry; Thomas Pressburger; Grigore Rosu (ASE, 2001)

Preface. - Klaus Havelund; Grigore Rosu (RV@CAV, 2001)

Monitoring Java Programs with Java PathExplorer. - Klaus Havelund; Grigore Rosu (RV@CAV, 2001)

Interpreting Abstract Interpretations in Membership Equational Logic. - Bernd Fischer 002; Grigore Rosu (RULE@PLI, 2001)

Equational axiomatizability for coalgebra. - Grigore Rosu (Theor. Comput. Sci., 2001)

A Total Approach to Partial Algebraic Specification. - José Meseguer 001; Grigore Rosu (ICALP, 2002)

Towards Certifying Domain-Specific Properties of Synthesized Code. - Grigore Rosu; Jon Whittle 001 (ASE, 2002)

On implementing behavioral rewriting. - Grigore Rosu (ACM SIGPLAN Workshop on Rule-Based Programming, 2002)

Synthesizing Monitors for Safety Properties. - Klaus Havelund; Grigore Rosu (TACAS, 2002)

Conditional Circular Coinductive Rewriting with Case Analysis. - Joseph A. Goguen; Kai Lin; Grigore Rosu (WADT, 2002)

Towards Behavioral Maude: Behavioral Membership Equational Logic. - José Meseguer 001; Grigore Rosu (CMCS, 2002)

Institution Morphisms. - Joseph A. Goguen; Grigore Rosu (Formal Aspects Comput., 2002)

Axiomatizability in Inclusive Equational Logics. - Grigore Rosu (Math. Struct. Comput. Sci., 2002)

Generating Optimal Linear Temporal Logic Monitors by Coinduction. - Koushik Sen; Grigore Rosu; Gul Agha (ASIAN, 2003)

Experiments with Test Case Generation and Runtime Analysis. - Cyrille Artho; Doron Drusinsky; Allen Goldberg; Klaus Havelund; Michael R. Lowry; Corina S. Pasareanu; Grigore Rosu; Willem Visser (Abstract State Machines, 2003)

Certifying Optimality of State Estimation Programs. - Grigore Rosu; Ram Prasad Venkatesan; Jon Whittle 001; Laurentiu Leustean (CAV, 2003)

Certifying and Synthesizing Membership Equational Proofs. - Grigore Rosu; Steven Eker; Patrick Lincoln; José Meseguer 001 (FME, 2003)

Certifying Measurement Unit Safety Polic. - Grigore Rosu; Feng Chen 006 (ASE, 2003)

Rule-Based Analysis of Dimensional Safety. - Feng Chen 006; Grigore Rosu; Ram Prasad Venkatesan (RTA, 2003)

Testing Extended Regular Language Membership Incrementally by Rewriting. - Grigore Rosu; Mahesh Viswanathan 001 (RTA, 2003)

Runtime safety analysis of multithreaded programs. - Koushik Sen; Grigore Rosu; Gul Agha (ESEC / SIGSOFT FSE, 2003)

Towards Monitoring-Oriented Programming: A Paradigm Combining Specification and Implementation. - Feng Chen 006; Grigore Rosu (RV@CAV, 2003)

Inductive Behavioral Proofs by Unhiding. - Grigore Rosu (CMCS, 2003)

Generating Optimal Monitors for Extended Regular Expressions. - Koushik Sen; Grigore Rosu (RV@CAV, 2003)

Formal JVM Code Analysis in JavaFAN. - Azadeh Farzan; José Meseguer 001; Grigore Rosu (AMAST, 2004)

Composing Hidden Information Modules over Inclusive Institutions. - Joseph A. Goguen; Grigore Rosu (Essays in Memory of Ole-Johan Dahl, 2004)

Rewriting Logic Semantics: From Language Specifications to Formal Analysis Tools. - José Meseguer 001; Grigore Rosu (IJCAR, 2004)

Formal Analysis of Java Programs in JavaFAN. - Azadeh Farzan; Feng Chen 006; José Meseguer 001; Grigore Rosu (CAV, 2004)

Extensional Theories and Rewriting. - Grigore Rosu (ICALP, 2004)

A Formal Monitoring-Based Framework for Software Development and Analysis. - Feng Chen 006; Marcelo d'Amorim; Grigore Rosu (ICFEM, 2004)

Efficient Decentralized Monitoring of Safety in Distributed Systems. - Koushik Sen; Abhay Vardhan; Gul Agha; Grigore Rosu (ICSE, 2004)

From Conditional to Unconditional Rewriting. - Grigore Rosu (WADT, 2004)

Monitoring Algorithms for Metric Temporal Logic Specifications. - Prasanna Thati; Grigore Rosu (RV@ETAPS, 2004)

Foreword - Selected Papers from the First International Workshop on Runtime Verification held in Paris, July 2001 (RV'01). - Klaus Havelund; Grigore Rosu (Formal Methods Syst. Des., 2004)

An Overview of the Runtime Verification Tool Java PathExplorer. - Klaus Havelund; Grigore Rosu (Formal Methods Syst. Des., 2004)

Efficient monitoring of safety properties. - Klaus Havelund; Grigore Rosu (Int. J. Softw. Tools Technol. Transf., 2004)

Behavioral abstraction is hiding information. - Grigore Rosu (Theor. Comput. Sci., 2004)

Behavioral Extensions of Institutions. - Andrei Popescu 001; Grigore Rosu (CALCO, 2005)

Efficient Monitoring of omega-Languages. - Marcelo d'Amorim; Grigore Rosu (CAV, 2005)

Formally Defining and Verifying Master/Slave Speculative Parallelization. - Pierre Salverda; Grigore Rosu; Craig B. Zilles (FM, 2005)

Detecting Errors in Multithreaded Programs by Generalized Predictive Analysis of Executions. - Koushik Sen; Grigore Rosu; Gul Agha (FMOODS, 2005)

A Tree Based Router Search Engine Architecture with Single Port Memories. - Florin Baboescu; Dean M. Tullsen; Grigore Rosu; Sumeet Singh (ISCA, 2005)

Java-MOP: A Monitoring Oriented Programming Environment for Java. - Feng Chen 006; Grigore Rosu (TACAS, 2005)

Computational Logical Frameworks and Generic Program Analysis Technologies. - José Meseguer 001; Grigore Rosu (VSTTE, 2005)

Rewriting-Based Techniques for Runtime Verification. - Grigore Rosu; Klaus Havelund (Autom. Softw. Eng., 2005)

Checking and Correcting Behaviors of Java Programs at Runtime with Java-MOP. - Feng Chen 006; Marcelo d'Amorim; Grigore Rosu (RV@CAV, 2005)

Foreword. - Klaus Havelund; Grigore Rosu (Formal Methods Syst. Des., 2005)

An Equational Specification for the Scheme Language. - Marcelo d'Amorim; Grigore Rosu (J. Univers. Comput. Sci., 2005)

Combining test case generation and runtime verification. - Cyrille Artho; Howard Barringer; Allen Goldberg; Klaus Havelund; Sarfraz Khurshid; Michael R. Lowry; Corina S. Pasareanu; Grigore Rosu; Koushik Sen; Willem Visser; Richard Washington (Theor. Comput. Sci., 2005)

Complete Categorical Deduction for Satisfaction as Injectivity. - Grigore Rosu (Essays Dedicated to Joseph A. Goguen, 2006)

Allen Linear (Interval) Temporal Logic - Translation to LTL and Monitor Synthesis. - Grigore Rosu; Saddek Bensalem (CAV, 2006)

Static Analysis to Enforce Safe Value Flow in Embedded Control Systems. - Sumant Kowshik; Grigore Rosu; Lui Sha (DSN, 2006)

Equality of streams is a Pi0 over 2-complete problem. - Grigore Rosu (ICFP, 2006)

Decentralized runtime analysis of multithreaded applications. - Koushik Sen; Abhay Vardhan; Gul Agha; Grigore Rosu (IPDPS, 2006)

Computationally Equivalent Elimination of Conditions. - Traian-Florin Serbanuta; Grigore Rosu (RTA, 2006)

Parametric and Termination-Sensitive Control Dependence. - Feng Chen 006; Grigore Rosu (SAS, 2006)

Rewriting Logic Systems. - Grit Denker; Carolyn L. Talcott; Grigore Rosu; Mark van den Brand; Steven Eker; Traian-Florin Serbanuta (WRLA, 2006)

A Rewrite Framework for Language Definitions and for Generation of Efficient Interpreters. - Mark Hills 001; Traian Serbanuta; Grigore Rosu (WRLA, 2006)

Online efficient predictive safety analysis of multithreaded programs. - Koushik Sen; Grigore Rosu; Gul Agha (Int. J. Softw. Tools Technol. Transf., 2006)

CIRC : A Circular Coinductive Prover. - Dorel Lucanu; Grigore Rosu (CALCO, 2007)

Parametric and Sliced Causality. - Feng Chen 006; Grigore Rosu (CAV, 2007)

07011 Executive Summary – Runtime Verification. - Bernd Finkbeiner; Klaus Havelund; Grigore Rosu; Oleg Sokolsky (Runtime Verification, 2007)

07011 Abstracts Collection – Runtime Verification. - Bernd Finkbeiner; Klaus Havelund; Grigore Rosu; Oleg Sokolsky (Runtime Verification, 2007)

On Formal Analysis of OO Languages Using Rewriting Logic: Designing for Performance. - Mark Hills 001; Grigore Rosu (FMOODS, 2007)

An Effective Algorithm for the Membership Problem for Extended Regular Expressions. - Grigore Rosu (FoSSaCS, 2007)

Mop: an efficient and generic runtime verification framework. - Feng Chen 006; Grigore Rosu (OOPSLA, 2007)

A rewriting approach to the design and evolution of object-oriented languages. - Mark Hills 001; Grigore Rosu (OOPSLA Companion, 2007)

KOOL: An Application of Rewriting Logic to Language Prototyping and Analysis. - Mark Hills 001; Grigore Rosu (RTA, 2007)

An instrumentation technique for online analysis of multithreaded programs. - Grigore Rosu; Koushik Sen (Concurr. Comput. Pract. Exp., 2007)

Regular Strategies as Proof Tactics for CIRC. - Dorel Lucanu; Grigore Rosu; Gheorghe Grigoras (WRS@RDP, 2007)

A Rewriting Logic Approach to Operational Semantics (Extended Abstract). - Traian-Florin Serbanuta; Grigore Rosu; José Meseguer 001 (SOS@LICS/ICALP, 2007)

Editorial. - Narciso Martí-Oliet; Grigore Rosu; Carolyn L. Talcott (High. Order Symb. Comput., 2007)

The rewriting logic semantics project. - José Meseguer 001; Grigore Rosu (Theor. Comput. Sci., 2007)

jPredictor: a predictive runtime analysis tool for java. - Feng Chen 006; Traian-Florin Serbanuta; Grigore Rosu (ICSE, 2008)

Defining and Executing P Systems with Structured Data in K. - Traian Serbanuta; Gheorghe Stefanescu; Grigore Rosu (Workshop on Membrane Computing, 2008)

Hardware Runtime Monitoring for Dependable COTS-Based Real-Time Embedded Systems. - Rodolfo Pellizzoni; Patrick O'Neil Meredith; Marco Caccamo; Grigore Rosu (RTSS, 2008)

Synthesizing Monitors for Safety Properties: This Time with Calls and Returns. - Grigore Rosu; Feng Chen 006; Thomas Ball 001 (RV, 2008)

A Rewriting Logic Approach to Type Inference. - Chucky Ellison; Traian-Florin Serbanuta; Grigore Rosu (WADT, 2008)

Towards a Module System for K. - Mark Hills 001; Grigore Rosu (WADT, 2008)

A Rewriting Logic Approach to Static Checking of Units of Measurement in C. - Mark Hills 001; Feng Chen 006; Grigore Rosu (RULE, 2008)

Preface. - Grigore Rosu (WRLA, 2008)

Dependent advice: a general approach to optimizing history-based aspects. - Eric Bodden; Feng Chen 006; Grigore Rosu (AOSD, 2009)

CIRC: A Behavioral Verification Tool Based on Circular Coinduction. - Dorel Lucanu; Eugen-Ioan Goriac; Georgiana Caltais; Grigore Rosu (CALCO, 2009)

Circular Coinduction: A Proof Theoretical Foundation. - Grigore Rosu; Dorel Lucanu (CALCO, 2009)

Circular Coinduction with Special Contexts. - Dorel Lucanu; Grigore Rosu (ICFEM, 2009)

Efficient Formalism-Independent Monitoring of Parametric Properties. - Feng Chen 006; Patrick O'Neil Meredith; Dongyun Jin; Grigore Rosu (ASE, 2009)

Runtime Verification of C Memory Safety. - Grigore Rosu; Wolfram Schulte; Traian-Florin Serbanuta (RV, 2009)

Parametric Trace Slicing and Monitoring. - Feng Chen 006; Grigore Rosu (TACAS, 2009)

A rewriting logic approach to operational semantics. - Traian-Florin Serbanuta; Grigore Rosu; José Meseguer 001 (Inf. Comput., 2009)

A semantic approach to interpolation. - Andrei Popescu 001; Traian-Florin Serbanuta; Grigore Rosu (Theor. Comput. Sci., 2009)

Matching Logic: An Alternative to Hoare/Floyd Logic. - Grigore Rosu; Chucky Ellison; Wolfram Schulte (AMAST, 2010)

Automating Coinduction with Case Analysis. - Eugen-Ioan Goriac; Dorel Lucanu; Grigore Rosu (ICFEM, 2010)

IMUnit: improved multithreaded unit testing. - Vilas Jagannath; Milos Gligoric 001; Dongyun Jin; Grigore Rosu; Darko Marinov (IWMSE@ICSE, 2010)

A formal executable semantics of Verilog. - Patrick O'Neil Meredith; Michael Katelman; José Meseguer 001; Grigore Rosu (MEMOCODE, 2010)

A Rewriting Logic Semantics Approach to Modular Program Analysis. - Mark Hills 001; Grigore Rosu (RTA, 2010)

Runtime Verification with the RV System. - Patrick O'Neil Meredith; Grigore Rosu (RV, 2010)

K-Maude: A Rewriting Based Tool for Semantics of Programming Languages. - Traian-Florin Serbanuta; Grigore Rosu (WRLA, 2010)

Efficient monitoring of parametric context-free patterns. - Patrick O'Neil Meredith; Dongyun Jin; Feng Chen 006; Grigore Rosu (Autom. Softw. Eng., 2010)

An overview of the K semantic framework. - Grigore Rosu; Traian-Florin Serbanuta (J. Log. Algebraic Methods Program., 2010)

Mining parametric specifications. - Choonghwan Lee; Feng Chen 006; Grigore Rosu (ICSE, 2011)

Matching logic: a new program verification approach. - Grigore Rosu; Andrei Stefanescu (ICSE, 2011)

Garbage collection for monitoring parametric properties. - Dongyun Jin; Patrick O'Neil Meredith; Dennis Griffith; Grigore Rosu (PLDI, 2011)

Improved multithreaded unit testing. - Vilas Jagannath; Milos Gligoric 001; Dongyun Jin; Qingzhou Luo; Grigore Rosu; Darko Marinov (SIGSOFT FSE, 2011)

Abstract Semantics for K Module Composition. - Codruta Gîrlea; Grigore Rosu (K, 2011)

K Overview and SIMPLE Case Study. - Grigore Rosu; Traian-Florin Serbanuta (K, 2011)

The K Primer (version 3.3). - Traian-Florin Serbanuta; Andrei Arusoaie; David Lazar; Chucky Ellison; Dorel Lucanu; Grigore Rosu (K, 2011)

Executing Formal Semantics with the K Tool. - David Lazar; Andrei Arusoaie; Traian-Florin Serbanuta; Chucky Ellison; Radu Mereuta; Dorel Lucanu; Grigore Rosu (FM, 2012)

From Hoare Logic to Matching Logic Reachability. - Grigore Rosu; Andrei Stefanescu (FM, 2012)

A Truly Concurrent Semantics for the K Framework Based on Graph Transformations. - Traian-Florin Serbanuta; Grigore Rosu (ICGT, 2012)

Towards a Unified Theory of Operational and Axiomatic Semantics. - Grigore Rosu; Andrei Stefanescu (ICALP (2), 2012)

JavaMOP: Efficient parametric runtime monitoring framework. - Dongyun Jin; Patrick O'Neil Meredith; Choonghwan Lee; Grigore Rosu (ICSE, 2012)

Checking reachability using matching logic. - Grigore Rosu; Andrei Stefanescu (OOPSLA, 2012)

Security-policy monitoring and enforcement with JavaMOP. - Soha Hussein; Patrick O'Neil Meredith; Grigore Rosu (PLAS, 2012)

An executable formal semantics of C with applications. - Chucky Ellison; Grigore Rosu (POPL, 2012)

Maximal Causal Models for Sequentially Consistent Systems. - Traian-Florin Serbanuta; Feng Chen 006; Grigore Rosu (RV, 2012)

Making Maude Definitions More Interactive. - Andrei Arusoaie; Traian-Florin Serbanuta; Chucky Ellison; Grigore Rosu (WRLA, 2012)

K Framework Distilled. - Dorel Lucanu; Traian-Florin Serbanuta; Grigore Rosu (WRLA, 2012)

Semantics and Algorithms for Parametric Monitoring - Grigore Rosu; Feng Chen 006 (Log. Methods Comput. Sci., 2012)

On Safety Properties and Their Monitoring. - Grigore Rosu (Sci. Ann. Comput. Sci., 2012)

Introduction to the special issue on runtime verification. - Oleg Sokolsky; Grigore Rosu (Formal Methods Syst. Des., 2012)

An overview of the MOP runtime verification framework. - Patrick O'Neil Meredith; Dongyun Jin; Dennis Griffith; Feng Chen 006; Grigore Rosu (Int. J. Softw. Tools Technol. Transf., 2012)

EnforceMOP: a runtime property enforcement system for multithreaded programs. - Qingzhou Luo; Grigore Rosu (ISSTA, 2013)

Efficient parametric runtime verification with deterministic string rewriting. - Patrick O'Neil Meredith; Grigore Rosu (ASE, 2013)

One-Path Reachability Logic. - Grigore Rosu; Andrei Stefanescu; Stefan Ciobaca; Brandon M. Moore (LICS, 2013)

Specifying Languages and Verifying Programs with K. - Grigore Rosu (SYNASC, 2013)

The rewriting logic semantics project: A progress report. - José Meseguer 001; Grigore Rosu (Inf. Comput., 2013)

Behavioral Rewrite Systems and Behavioral Productivity. - Grigore Rosu; Dorel Lucanu (Specification, Algebra, and Software, 2014)

A Language-Independent Proof System for Mutual Program Equivalence. - Stefan Ciobaca; Dorel Lucanu; Vlad Rusu; Grigore Rosu (ICFEM, 2014)

Maximal sound predictive race detection with control flow abstraction. - Jeff Huang 001; Patrick O'Neil Meredith; Grigore Rosu (PLDI, 2014)

ROSRV: Runtime Verification for Robots. - Jeff Huang 001; Cansu Erdogan; Yi Zhang; Brandon M. Moore; Qingzhou Luo; Aravind Sundaresan; Grigore Rosu (RV, 2014)

RV-Monitor: Efficient Parametric Runtime Verification with Simultaneous Properties. - Qingzhou Luo; Yi Zhang; Choonghwan Lee; Dongyun Jin; Patrick O'Neil Meredith; Traian-Florin Serbanuta; Grigore Rosu (RV, 2014)

A Theoretical Foundation for Programming Languages Aggregation. - Stefan Ciobaca; Dorel Lucanu; Vlad Rusu; Grigore Rosu (WADT, 2014)

On the complexity of stream equality. - Jörg Endrullis; Dimitri Hendriks; Rena Bakhshi; Grigore Rosu (J. Funct. Program., 2014)

From Rewriting Logic, to Programming Language Semantics, to Program Verification. - Grigore Rosu (Logic, Rewriting, and Concurrency, 2015)

GPredict: Generic Predictive Concurrency Analysis. - Jeff Huang 001; Qingzhou Luo; Grigore Rosu (ICSE (1), 2015)

Evolution-Aware Monitoring-Oriented Programming. - Owolabi Legunsen; Darko Marinov; Grigore Rosu (ICSE (2), 2015)

Defining the undefinedness of C. - Chris Hathhorn; Chucky Ellison; Grigore Rosu (PLDI, 2015)

KJS: a complete formal semantics of JavaScript. - Daejun Park 001; Andrei Stefanescu; Grigore Rosu (PLDI, 2015)

K-Java: A Complete Semantics of Java. - Denis Bogdanas; Grigore Rosu (POPL, 2015)

Matching Logic - Extended Abstract (Invited Talk). - Grigore Rosu (RTA, 2015)

RV-Android: Efficient Parametric Android Runtime Verification, a Brief Tutorial. - Philip Daian; Yliès Falcone; Patrick O'Neil Meredith; Traian-Florin Serbanuta; Shinichi Shiraishi; Akihito Iwai; Grigore Rosu (RV, 2015)

Term-generic logic. - Andrei Popescu 001; Grigore Rosu (Theor. Comput. Sci., 2015)

Towards a mathbb K K ool Future. - Dorel Lucanu; Traian-Florin Serbanuta; Grigore Rosu (Theory and Practice of Formal Methods, 2016)

RV-Match: Practical Semantics-Based Program Analysis. - Dwight Guth; Chris Hathhorn; Manasvi Saxena; Grigore Rosu (CAV (1), 2016)

How good are the specs? a study of the bug-finding effectiveness of existing Java API specifications. - Owolabi Legunsen; Wajih Ul Hassan; Xinyue Xu; Grigore Rosu; Darko Marinov (ASE, 2016)

Semantics-based program verifiers for all languages. - Andrei Stefanescu; Daejun Park 001; Shijiao Yuwen; Yilong Li; Grigore Rosu (OOPSLA, 2016)

Runtime Verification at Work: A Tutorial. - Philip Daian; Dwight Guth; Chris Hathhorn; Yilong Li; Edgar Pek; Manasvi Saxena; Traian-Florin Serbanuta; Grigore Rosu (RV, 2016)

A language-independent proof system for full program equivalence. - Stefan Ciobaca; Dorel Lucanu; Vlad Rusu; Grigore Rosu (Formal Aspects Comput., 2016)

Language definitions as rewrite theories. - Vlad Rusu; Dorel Lucanu; Traian-Florin Serbanuta; Andrei Arusoaie; Andrei Stefanescu; Grigore Rosu (J. Log. Algebraic Methods Program., 2016)

Matching Logic. - Grigore Rosu (Log. Methods Comput. Sci., 2017)

𝕂: A Semantic Framework for Programming Languages and Formal Analysis Tools. - Grigore Rosu (Dependable Software Systems Engineering, 2017)

KEVM: A Complete Formal Semantics of the Ethereum Virtual Machine. - Everett Hildenbrandt; Manasvi Saxena; Nishant Rodrigues; Xiaoran Zhu; Philip Daian; Dwight Guth; Brandon M. Moore; Daejun Park 001; Yi Zhang; Andrei Stefanescu; Grigore Rosu (CSF, 2018)

Program Verification by Coinduction. - Brandon M. Moore; Lucas Peña; Grigore Rosu (ESOP, 2018)

A Language-Independent Approach to Smart Contract Verification. - Xiaohong Chen 002; Daejun Park 001; Grigore Rosu (ISoLA (4), 2018)

A Language-Independent Program Verification Framework. - Xiaohong Chen 002; Grigore Rosu (ISoLA (2), 2018)

Formal Design, Implementation and Verification of Blockchain Languages (Invited Talk). - Grigore Rosu (FSCD, 2018)

Runtime Verification - 17 Years Later. - Klaus Havelund; Grigore Rosu (RV, 2018)

A formal verification tool for Ethereum VM bytecode. - Daejun Park 001; Yi Zhang; Manasvi Saxena; Philip Daian; Grigore Rosu (ESEC/SIGSOFT FSE, 2018)

P4K: A Formal Semantics of P4 and Applications. - Ali Kheradmand; Grigore Rosu (CoRR, 2018)

Finite-trace linear temporal logic: coinductive completeness. - Grigore Rosu (Formal Methods Syst. Des., 2018)

Matching mu-Logic: Foundation of K Framework (Invited Paper). - Xiaohong Chen 002; Grigore Rosu (CALCO, 2019)

Towards a Verified Model of the Algorand Consensus Protocol in Coq. - Musab A. Alturki; Jing Chen; Victor Luchangco; Brandon M. Moore; Karl Palmskog; Lucas Peña; Grigore Rosu (FM Workshops (1), 2019)

Statistical Model Checking of RANDAO's Resilience to Pre-computed Reveal Strategies. - Musab A. Alturki; Grigore Rosu (FM Workshops (1), 2019)

IELE: A Rigorously Designed Language and Tool Ecosystem for the Blockchain. - Theodoros Kasampalis; Dwight Guth; Brandon M. Moore; Traian-Florin Serbanuta; Yi Zhang; Daniele Filaretti; Virgil Nicolae Serbanuta; Ralph Johnson; Grigore Rosu (FM, 2019)

Techniques for Evolution-Aware Runtime Verification. - Owolabi Legunsen; Yi Zhang; Milica Hadzi-Tanovic; Grigore Rosu; Darko Marinov (ICST, 2019)

Matching μ-Logic. - Xiaohong Chen 002; Grigore Rosu (LICS, 2019)

A complete formal semantics of x86-64 user-level instruction set architecture. - Sandeep Dasgupta; Daejun Park 001; Theodoros Kasampalis; Vikram S. Adve; Grigore Rosu (PLDI, 2019)

$ mathbb {K}$ - A Semantic Framework for Programming Languages and Formal Analysis. - Xiaohong Chen 002; Grigore Rosu (SETSS, 2019)

How effective are existing Java API specifications for finding bugs during runtime verification? - Owolabi Legunsen; Nader Al Awar; Xinyue Xu; Wajih Ul Hassan; Grigore Rosu; Darko Marinov (Autom. Softw. Eng., 2019)

All-Path Reachability Logic. - Andrei Stefanescu; Stefan Ciobaca; Radu Mereuta; Brandon M. Moore; Traian-Florin Serbanuta; Grigore Rosu (Log. Methods Comput. Sci., 2019)

Dealing With C's Original Sin. - Chris Hathhorn; Grigore Rosu (IEEE Softw., 2019)

First international Competition on Runtime Verification: rules, benchmarks, tools, and final results of CRV 2014. - Ezio Bartocci; Yliès Falcone; Borzoo Bonakdarpour; Christian Colombo 001; Normann Decker; Klaus Havelund; Yogi Joshi; Felix Klaedtke; Reed Milewicz; Giles Reger; Grigore Rosu; Julien Signoles; et al. (Int. J. Softw. Tools Technol. Transf., 2019)

Runtime Verification Past Experiences and Future Projections. - Klaus Havelund; Giles Reger; Grigore Rosu (Computing and Software Science, 2019)

End-to-End Formal Verification of Ethereum 2.0 Deposit Smart Contract. - Daejun Park 001; Yi Zhang; Grigore Rosu (CAV (1), 2020)

Formal Design, Implementation and Verification of Blockchain Languages Using K (Invited Talk). - Grigore Rosu (FMBC@CAV, 2020)

Matching logic: the foundation of the K framework (invited talk). - Grigore Rosu; Xiaohong Chen 002 (CPP, 2020)

Formalizing Correct-by-Construction Casper in Coq. - Elaine Li; Traian Serbanuta; Denisa Diaconescu; Vlad Zamfir; Grigore Rosu (IEEE ICBC, 2020)

Connecting Constrained Constructor Patterns and Matching Logic. - Xiaohong Chen 002; Dorel Lucanu; Grigore Rosu (WRLA@ETAPS, 2020)

Specification of the Giskard Consensus Protocol. - Elaine Li; Karl Palmskog; Mircea Sebe; Grigore Rosu (CoRR, 2020)

Towards a unified proof framework for automated fixpoint reasoning using matching logic. - Xiaohong Chen 002; Minh-Thai Trinh; Nishant Rodrigues; Lucas Peña; Grigore Rosu (Proc. ACM Program. Lang., 2020)

A general approach to define binders using matching logic. - Xiaohong Chen 002; Grigore Rosu (Proc. ACM Program. Lang., 2020)

Language-parametric compiler validation with application to LLVM. - Theodoros Kasampalis; Daejun Park 001; Zhengyao Lin; Vikram S. Adve; Grigore Rosu (ASPLOS, 2021)

The K Vision for the Future of Programming Language Design and Analysis. - Xiaohong Chen 002; Grigore Rosu (Formal Methods in Outer Space, 2021)

Towards a Trustworthy Semantics-Based Language Framework via Proof Generation. - Xiaohong Chen 002; Zhengyao Lin; Minh-Thai Trinh; Grigore Rosu (CAV (2), 2021)

Rigorous Methods for Smart Contracts (Dagstuhl Seminar 21431). - Nikolaj S. Bjørner; Maria Christakis; Matteo Maffei; Grigore Rosu (Dagstuhl Reports, 2021)

Matching logic explained. - Xiaohong Chen 002; Dorel Lucanu; Grigore Rosu (J. Log. Algebraic Methods Program., 2021)

Towards a Trustworthy Semantics-Based Language Framework via Proof Generation. - Xiaohong Chen 002; Zhengyao Lin; Minh-Thai Trinh; Grigore Rosu (Zenodo, 2021)

Towards a Trustworthy Semantics-Based Language Framework via Proof Generation. - Xiaohong Chen 002; Zhengyao Lin; Minh-Thai Trinh; Grigore Rosu (Zenodo, 2021)

Towards a Trustworthy Semantics-Based Language Framework via Proof Generation. - Xiaohong Chen 002; Zhengyao Lin; Minh-Thai Trinh; Grigore Rosu (Zenodo, 2021)

Generating Proof Certificates for a Language-Agnostic Deductive Program Verifier. - Zhengyao Lin; Xiaohong Chen 002; Minh-Thai Trinh; John Wang; Grigore Rosu (Zenodo, 2022)

Generating Proof Certificates for a Language-Agnostic Deductive Program Verifier. - Zhengyao Lin; Xiaohong Chen 002; Minh-Thai Trinh; John Wang; Grigore Rosu (Zenodo, 2022)

Generating Proof Certificates for a Language-Agnostic Deductive Program Verifier. - Zhengyao Lin; Xiaohong Chen 002; Minh-Thai Trinh; John Wang; Grigore Rosu (Zenodo, 2022)

Generating Proof Certificates for a Language-Agnostic Deductive Program Verifier. - Zhengyao Lin; Xiaohong Chen 002; Minh-Thai Trinh; John Wang; Grigore Rosu (Zenodo, 2022)

Capturing constrained constructor patterns in matching logic. - Xiaohong Chen 002; Dorel Lucanu; Grigore Rosu (J. Log. Algebraic Methods Program., 2023)

Generating Proof Certificates for a Language-Agnostic Deductive Program Verifier. - Zhengyao Lin; Xiaohong Chen 002; Minh-Thai Trinh; John Wang; Grigore Rosu (Proc. ACM Program. Lang., 2023)

A Logical Treatment of Finite Automata. - Nishant Rodrigues; Mircea Sebe; Xiaohong Chen 002; Grigore Rosu (TACAS (1), 2024)

FastSet: Parallel Claim Settlement. - Xiaohong Chen 002; Grigore Rosu (CoRR, 2025)