| 2026 | FOSSACS | $\mathbb {K}$ Definitions as Matching Logic Theories, Formally. | Xiaohong Chen, Horatiu Cheval, Dorel Lucanu, Grigore Rosu |
| 2024 | TACAS | A Logical Treatment of Finite Automata. | Nishant Rodrigues, Mircea Sebe, Xiaohong Chen, Grigore Rosu |
| 2021 | ASPLOS | Language-parametric compiler validation with application to LLVM. | Theodoros Kasampalis, Daejun Park, Zhengyao Lin, Vikram S. Adve, Grigore Rosu |
| 2021 | CAV | Towards a Trustworthy Semantics-Based Language Framework via Proof Generation. | Xiaohong Chen, Zhengyao Lin, Minh-Thai Trinh, Grigore Rosu |
| 2020 | CAV | End-to-End Formal Verification of Ethereum 2.0 Deposit Smart Contract. | Daejun Park, Yi Zhang, Grigore Rosu |
| 2020 | CAV | Formal Design, Implementation and Verification of Blockchain Languages Using K (Invited Talk). | Grigore Rosu |
| 2020 | CPP | Matching logic: the foundation of the K framework (invited talk). | Grigore Rosu, Xiaohong Chen |
| 2019 | CALCO | Matching mu-Logic: Foundation of K Framework (Invited Paper). | Xiaohong Chen, Grigore Rosu |
| 2019 | FM | Towards a Verified Model of the Algorand Consensus Protocol in Coq. | Musab A. Alturki, Jing Chen, Victor Luchangco, Brandon M. Moore, Karl Palmskog, Lucas Pea, Grigore Rosu |
| 2019 | FM | Statistical Model Checking of RANDAO's Resilience to Pre-computed Reveal Strategies. | Musab A. Alturki, Grigore Rosu |
| 2019 | FM | 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 |
| 2019 | ICST | Techniques for Evolution-Aware Runtime Verification. | Owolabi Legunsen, Yi Zhang, Milica Hadzi-Tanovic, Grigore Rosu, Darko Marinov |
| 2019 | LICS | Matching μ-Logic. | Xiaohong Chen, Grigore Rosu |
| 2019 | PLDI | A complete formal semantics of x86-64 user-level instruction set architecture. | Sandeep Dasgupta, Daejun Park, Theodoros Kasampalis, Vikram S. Adve, Grigore Rosu |
| 2018 | ESOP | Program Verification by Coinduction. | Brandon M. Moore, Lucas Pea, Grigore Rosu |
| 2018 | ISoLA | A Language-Independent Approach to Smart Contract Verification. | Xiaohong Chen, Daejun Park, Grigore Rosu |
| 2018 | ISoLA | A Language-Independent Program Verification Framework. | Xiaohong Chen, Grigore Rosu |
| 2018 | RV | Runtime Verification - 17 Years Later. | Klaus Havelund, Grigore Rosu |
| 2016 | CAV | RV-Match: Practical Semantics-Based Program Analysis. | Dwight Guth, Chris Hathhorn, Manasvi Saxena, Grigore Rosu |
| 2016 | OOPSLA | Semantics-based program verifiers for all languages. | Andrei Stefanescu, Daejun Park, Shijiao Yuwen, Yilong Li, Grigore Rosu |
| 2016 | RV | Runtime Verification at Work: A Tutorial. | Philip Daian, Dwight Guth, Chris Hathhorn, Yilong Li, Edgar Pek, Manasvi Saxena, Traian-Florin Serbanuta, Grigore Rosu |
| 2016 | RV | Finite-Trace Linear Temporal Logic: Coinductive Completeness. | Grigore Rosu |
| 2015 | ICSE | GPredict: Generic Predictive Concurrency Analysis. | Jeff Huang, Qingzhou Luo, Grigore Rosu |
| 2015 | ICSE | Evolution-Aware Monitoring-Oriented Programming. | Owolabi Legunsen, Darko Marinov, Grigore Rosu |
| 2015 | PLDI | Defining the undefinedness of C. | Chris Hathhorn, Chucky Ellison, Grigore Rosu |
| 2015 | PLDI | KJS: a complete formal semantics of JavaScript. | Daejun Park, Andrei Stefanescu, Grigore Rosu |
| 2015 | POPL | K-Java: A Complete Semantics of Java. | Denis Bogdanas, Grigore Rosu |
| 2015 | RV | RV-Android: Efficient Parametric Android Runtime Verification, a Brief Tutorial. | Philip Daian, Ylis Falcone, Patrick O'Neil Meredith, Traian-Florin Serbanuta, Shinichi Shiraishi, Akihito Iwai, Grigore Rosu |
| 2014 | ICFEM | A Language-Independent Proof System for Mutual Program Equivalence. | Stefan Ciobaca, Dorel Lucanu, Vlad Rusu, Grigore Rosu |
| 2014 | PLDI | Maximal sound predictive race detection with control flow abstraction. | Jeff Huang, Patrick O'Neil Meredith, Grigore Rosu |
| 2014 | RV | ROSRV: Runtime Verification for Robots. | Jeff Huang, Cansu Erdogan, Yi Zhang, Brandon M. Moore, Qingzhou Luo, Aravind Sundaresan, Grigore Rosu |
| 2014 | RV | 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 |
| 2013 | ISSTA | EnforceMOP: a runtime property enforcement system for multithreaded programs. | Qingzhou Luo, Grigore Rosu |
| 2013 | LICS | One-Path Reachability Logic. | Grigore Rosu, Andrei Stefanescu, Stefan Ciobaca, Brandon M. Moore |
| 2013 | SYNASC | Specifying Languages and Verifying Programs with K. | Grigore Rosu |
| 2012 | FM | Executing Formal Semantics with the K Tool. | David Lazar, Andrei Arusoaie, Traian-Florin Serbanuta, Chucky Ellison, Radu Mereuta, Dorel Lucanu, Grigore Rosu |
| 2012 | FM | From Hoare Logic to Matching Logic Reachability. | Grigore Rosu, Andrei Stefanescu |
| 2012 | ICALP | Towards a Unified Theory of Operational and Axiomatic Semantics. | Grigore Rosu, Andrei Stefanescu |
| 2012 | ICSE | JavaMOP: Efficient parametric runtime monitoring framework. | Dongyun Jin, Patrick O'Neil Meredith, Choonghwan Lee, Grigore Rosu |
| 2012 | OOPSLA | Checking reachability using matching logic. | Grigore Rosu, Andrei Stefanescu |
| 2012 | PLDI | Security-policy monitoring and enforcement with JavaMOP. | Soha Hussein, Patrick O'Neil Meredith, Grigore Rosu |
| 2012 | POPL | An executable formal semantics of C with applications. | Chucky Ellison, Grigore Rosu |
| 2012 | RV | Maximal Causal Models for Sequentially Consistent Systems. | Traian-Florin Serbanuta, Feng Chen, Grigore Rosu |
| 2011 | FCT | The Rewriting Logic Semantics Project: A Progress Report. | Jos Meseguer, Grigore Rosu |
| 2011 | ICSE | Mining parametric specifications. | Choonghwan Lee, Feng Chen, Grigore Rosu |
| 2011 | ICSE | Matching logic: a new program verification approach. | Grigore Rosu, Andrei Stefanescu |
| 2011 | PLDI | Garbage collection for monitoring parametric properties. | Dongyun Jin, Patrick O'Neil Meredith, Dennis Griffith, Grigore Rosu |
| 2010 | ICFEM | Automating Coinduction with Case Analysis. | Eugen-Ioan Goriac, Dorel Lucanu, Grigore Rosu |
| 2010 | ICSE | IMUnit: improved multithreaded unit testing. | Vilas Jagannath, Milos Gligoric, Dongyun Jin, Grigore Rosu, Darko Marinov |
| 2010 | MEMOCODE | A formal executable semantics of Verilog. | Patrick O'Neil Meredith, Michael Katelman, Jos Meseguer, Grigore Rosu |
| 2010 | RV | Runtime Verification with the RV System. | Patrick O'Neil Meredith, Grigore Rosu |
| 2009 | CALCO | CIRC: A Behavioral Verification Tool Based on Circular Coinduction. | Dorel Lucanu, Eugen-Ioan Goriac, Georgiana Caltais, Grigore Rosu |
| 2009 | CALCO | Circular Coinduction: A Proof Theoretical Foundation. | Grigore Rosu, Dorel Lucanu |
| 2009 | ICFEM | Circular Coinduction with Special Contexts. | Dorel Lucanu, Grigore Rosu |
| 2009 | RV | Runtime Verification of C Memory Safety. | Grigore Rosu, Wolfram Schulte, Traian-Florin Serbanuta |
| 2009 | TACAS | Parametric Trace Slicing and Monitoring. | Feng Chen, Grigore Rosu |
| 2008 | ICSE | jPredictor: a predictive runtime analysis tool for java. | Feng Chen, Traian-Florin Serbanuta, Grigore Rosu |
| 2008 | RTSS | Hardware Runtime Monitoring for Dependable COTS-Based Real-Time Embedded Systems. | Rodolfo Pellizzoni, Patrick O'Neil Meredith, Marco Caccamo, Grigore Rosu |
| 2008 | RV | Synthesizing Monitors for Safety Properties: This Time with Calls and Returns. | Grigore Rosu, Feng Chen, Thomas Ball |
| 2007 | CALCO | CIRC : A Circular Coinductive Prover. | Dorel Lucanu, Grigore Rosu |
| 2007 | CAV | Parametric and Sliced Causality. | Feng Chen, Grigore Rosu |
| 2007 | FOSSACS | An Effective Algorithm for the Membership Problem for Extended Regular Expressions. | Grigore Rosu |
| 2007 | OOPSLA | Mop: an efficient and generic runtime verification framework. | Feng Chen, Grigore Rosu |
| 2007 | OOPSLA | A rewriting approach to the design and evolution of object-oriented languages. | Mark Hills, Grigore Rosu |
| 2006 | CAV | Allen Linear (Interval) Temporal Logic - Translation to LTL and Monitor Synthesis. | Grigore Rosu, Saddek Bensalem |
| 2006 | DSN | Static Analysis to Enforce Safe Value Flow in Embedded Control Systems. | Sumant Kowshik, Grigore Rosu, Lui Sha |
| 2006 | FOSSACS | A Semantic Approach to Interpolation. | Andrei Popescu, Traian Serbanuta, Grigore Rosu |
| 2006 | ICFP | Equality of streams is a Pi0 over 2-complete problem. | Grigore Rosu |
| 2006 | SAS | Parametric and Termination-Sensitive Control Dependence. | Feng Chen, Grigore Rosu |
| 2005 | CALCO | Behavioral Extensions of Institutions. | Andrei Popescu, Grigore Rosu |
| 2005 | CAV | Efficient Monitoring of omega-Languages. | Marcelo d'Amorim, Grigore Rosu |
| 2005 | FM | Formally Defining and Verifying Master/Slave Speculative Parallelization. | Pierre Salverda, Grigore Rosu, Craig B. Zilles |
| 2005 | ISCA | A Tree Based Router Search Engine Architecture with Single Port Memories. | Florin Baboescu, Dean M. Tullsen, Grigore Rosu, Sumeet Singh |
| 2005 | TACAS | Java-MOP: A Monitoring Oriented Programming Environment for Java. | Feng Chen, Grigore Rosu |
| 2004 | CADE | Rewriting Logic Semantics: From Language Specifications to Formal Analysis Tools. | Jos Meseguer, Grigore Rosu |
| 2004 | CAV | Formal Analysis of Java Programs in JavaFAN. | Azadeh Farzan, Feng Chen, Jos Meseguer, Grigore Rosu |
| 2004 | ICALP | Extensional Theories and Rewriting. | Grigore Rosu |
| 2004 | ICFEM | A Formal Monitoring-Based Framework for Software Development and Analysis. | Feng Chen, Marcelo d'Amorim, Grigore Rosu |
| 2004 | ICSE | Efficient Decentralized Monitoring of Safety in Distributed Systems. | Koushik Sen, Abhay Vardhan, Gul Agha, Grigore Rosu |
| 2004 | TACAS | Online Efficient Predictive Safety Analysis of Multithreaded Programs. | Koushik Sen, Grigore Rosu, Gul Agha |
| 2003 | CAV | Certifying Optimality of State Estimation Programs. | Grigore Rosu, Ram Prasad Venkatesan, Jon Whittle, Laurentiu Leustean |
| 2003 | FM | Certifying and Synthesizing Membership Equational Proofs. | Grigore Rosu, Steven Eker, Patrick Lincoln, Jos Meseguer |
| 2002 | ICALP | A Total Approach to Partial Algebraic Specification. | Jos Meseguer, Grigore Rosu |
| 2002 | TACAS | Synthesizing Monitors for Safety Properties. | Klaus Havelund, Grigore Rosu |
| 2001 | CSL | Complete Categorical Equational Deduction. | Grigore Rosu |
| 1999 | FM | Hiding More of Hidden Algebra. | Joseph A. Goguen, Grigore Rosu |