Grigore Rosu

ORCID

Publication Activity (10 Years)

Years Active: 1994-2024
Publications (10 Years): 49

Top Venues

CoRR

PLDI

Electron. Notes Theor. Comput. Sci.

Publications

Nishant Rodrigues, Mircea Sebe, Xiaohong Chen, Grigore Rosu
A Logical Treatment of Finite Automata. TACAS (1) (2024)
Zhengyao Lin, Xiaohong Chen, Minh-Thai Trinh, John Wang, Grigore Rosu
Generating Proof Certificates for a Language-Agnostic Deductive Program Verifier. Proc. ACM Program. Lang. 7 (OOPSLA1) (2023)
Xiaohong Chen, Dorel Lucanu, Grigore Rosu
Capturing constrained constructor patterns in matching logic. J. Log. Algebraic Methods Program. 130 (2023)
Xiaohong Chen, Dorel Lucanu, Grigore Rosu
Matching logic explained. J. Log. Algebraic Methods Program. 120 (2021)
Nikolaj S. Bjørner, Maria Christakis, Matteo Maffei, Grigore Rosu
Rigorous Methods for Smart Contracts (Dagstuhl Seminar 21431). Dagstuhl Reports 11 (9) (2021)
Theodoros Kasampalis, Daejun Park, Zhengyao Lin, Vikram S. Adve, Grigore Rosu
Language-parametric compiler validation with application to LLVM. ASPLOS (2021)
Xiaohong Chen, Zhengyao Lin, Minh-Thai Trinh, Grigore Rosu
Towards a Trustworthy Semantics-Based Language Framework via Proof Generation. CAV (2) (2021)
Xiaohong Chen, Grigore Rosu
The K Vision for the Future of Programming Language Design and Analysis. Formal Methods in Outer Space (2021)
Xiaohong Chen, Dorel Lucanu, Grigore Rosu
Connecting Constrained Constructor Patterns and Matching Logic. WRLA@ETAPS (2020)
Elaine Li, Karl Palmskog, Mircea Sebe, Grigore Rosu
Specification of the Giskard Consensus Protocol. CoRR (2020)
Grigore Rosu, Xiaohong Chen
Matching logic: the foundation of the K framework (invited talk). CPP (2020)
Daejun Park, Yi Zhang, Grigore Rosu
End-to-End Formal Verification of Ethereum 2.0 Deposit Smart Contract. CAV (1) (2020)
Xiaohong Chen, Grigore Rosu
A general approach to define binders using matching logic. Proc. ACM Program. Lang. 4 (ICFP) (2020)
Xiaohong Chen, Minh-Thai Trinh, Nishant Rodrigues, Lucas Peña, Grigore Rosu
Towards a unified proof framework for automated fixpoint reasoning using matching logic. Proc. ACM Program. Lang. 4 (OOPSLA) (2020)
Elaine Li, Traian Serbanuta, Denisa Diaconescu, Vlad Zamfir, Grigore Rosu
Formalizing Correct-by-Construction Casper in Coq. IEEE ICBC (2020)
Grigore Rosu
Formal Design, Implementation and Verification of Blockchain Languages Using K (Invited Talk). FMBC@CAV (2020)
Musab A. Alturki, Grigore Rosu
Statistical Model Checking of RANDAO's Resilience to Pre-computed Reveal Strategies. FM Workshops (1) (2019)
Xiaohong Chen, Grigore Rosu
Matching mu-Logic: Foundation of K Framework (Invited Paper). CALCO (2019)
Owolabi Legunsen, Nader Al Awar, Xinyue Xu, Wajih Ul Hassan, Grigore Rosu, Darko Marinov
How effective are existing Java API specifications for finding bugs during runtime verification? Autom. Softw. Eng. 26 (4) (2019)
Owolabi Legunsen, Yi Zhang, Milica Hadzi-Tanovic, Grigore Rosu, Darko Marinov
Techniques for Evolution-Aware Runtime Verification. ICST (2019)
Sandeep Dasgupta, Daejun Park, Theodoros Kasampalis, Vikram S. Adve, Grigore Rosu
A complete formal semantics of x86-64 user-level instruction set architecture. PLDI (2019)
Musab A. Alturki, Jing Chen, Victor Luchangco, Brandon M. Moore, Karl Palmskog, Lucas Peña, Grigore Rosu
Towards a Verified Model of the Algorand Consensus Protocol in Coq. FM Workshops (1) (2019)
Theodoros Kasampalis, Dwight Guth, Brandon M. Moore, Traian-Florin Serbanuta, Yi Zhang, Daniele Filaretti, Virgil Nicolae Serbanuta, Ralph Johnson, Grigore Rosu
IELE: A Rigorously Designed Language and Tool Ecosystem for the Blockchain. FM (2019)
Chris Hathhorn, Grigore Rosu
Dealing With C's Original Sin. IEEE Softw. 36 (5) (2019)
Musab A. Alturki, Jing Chen, Victor Luchangco, Brandon M. Moore, Karl Palmskog, Lucas Peña, Grigore Rosu
Towards a Verified Model of the Algorand Consensus Protocol in Coq. CoRR (2019)
Ezio Bartocci, Yliès Falcone, Borzoo Bonakdarpour, Christian Colombo, Normann Decker, Klaus Havelund, Yogi Joshi, Felix Klaedtke, Reed Milewicz, Giles Reger, Grigore Rosu, Julien Signoles, Daniel Thoma, Eugen Zalinescu, Yi Zhang
First international Competition on Runtime Verification: rules, benchmarks, tools, and final results of CRV 2014. Int. J. Softw. Tools Technol. Transf. 21 (1) (2019)
Xiaohong Chen, Grigore Rosu
$\mathbb {K}$ - A Semantic Framework for Programming Languages and Formal Analysis. SETSS (2019)
Andrei Stefanescu, Stefan Ciobaca, Radu Mereuta, Brandon M. Moore, Traian-Florin Serbanuta, Grigore Rosu
All-Path Reachability Logic. Log. Methods Comput. Sci. 15 (2) (2019)
Xiaohong Chen, Grigore Rosu
Matching μ-Logic. LICS (2019)
Grigore Rosu
Finite-trace linear temporal logic: coinductive completeness. Formal Methods Syst. Des. 53 (1) (2018)
Brandon M. Moore, Lucas Peña, Grigore Rosu
Program Verification by Coinduction. ESOP (2018)
Klaus Havelund, Grigore Rosu
Runtime Verification - 17 Years Later. RV (2018)
Andrei Stefanescu, Stefan Ciobaca, Radu Mereuta, Brandon M. Moore, Traian-Florin Serbanuta, Grigore Rosu
All-Path Reachability Logic. CoRR (2018)
Ali Kheradmand, Grigore Rosu
P4K: A Formal Semantics of P4 and Applications. CoRR (2018)
Daejun Park, Yi Zhang, Manasvi Saxena, Philip Daian, Grigore Rosu
A formal verification tool for Ethereum VM bytecode. ESEC/SIGSOFT FSE (2018)
Everett Hildenbrandt, Manasvi Saxena, Nishant Rodrigues, Xiaoran Zhu, Philip Daian, Dwight Guth, Brandon M. Moore, Daejun Park, Yi Zhang, Andrei Stefanescu, Grigore Rosu
KEVM: A Complete Formal Semantics of the Ethereum Virtual Machine. CSF (2018)
Xiaohong Chen, Daejun Park, Grigore Rosu
A Language-Independent Approach to Smart Contract Verification. ISoLA (4) (2018)
Xiaohong Chen, Grigore Rosu
A Language-Independent Program Verification Framework. ISoLA (2) (2018)
Grigore Rosu
Formal Design, Implementation and Verification of Blockchain Languages (Invited Talk). FSCD (2018)
Grigore Rosu
Matching Logic. Log. Methods Comput. Sci. 13 (4) (2017)
Grigore Rosu
Matching Logic. CoRR (2017)
Vlad Rusu, Dorel Lucanu, Traian-Florin Serbanuta, Andrei Arusoaie, Andrei Stefanescu, Grigore Rosu
Language definitions as rewrite theories. J. Log. Algebraic Methods Program. 85 (1) (2016)
Dwight Guth, Chris Hathhorn, Manasvi Saxena, Grigore Rosu
RV-Match: Practical Semantics-Based Program Analysis. CAV (1) (2016)
Dorel Lucanu, Traian-Florin Serbanuta, Grigore Rosu
Towards a \mathbb K K ool Future. Theory and Practice of Formal Methods (2016)
Andrei Stefanescu, Daejun Park, Shijiao Yuwen, Yilong Li, Grigore Rosu
Semantics-based program verifiers for all languages. OOPSLA (2016)
Stefan Ciobaca, Dorel Lucanu, Vlad Rusu, Grigore Rosu
A language-independent proof system for full program equivalence. Formal Aspects Comput. 28 (3) (2016)
Philip Daian, Dwight Guth, Chris Hathhorn, Yilong Li, Edgar Pek, Manasvi Saxena, Traian-Florin Serbanuta, Grigore Rosu
Runtime Verification at Work: A Tutorial. RV (2016)
Grigore Rosu
Finite-Trace Linear Temporal Logic: Coinductive Completeness. RV (2016)
Owolabi Legunsen, Wajih Ul Hassan, Xinyue Xu, Grigore Rosu, Darko Marinov
How good are the specs? a study of the bug-finding effectiveness of existing Java API specifications. ASE (2016)
Chris Hathhorn, Chucky Ellison, Grigore Rosu
Defining the undefinedness of C. PLDI (2015)
Grigore Rosu
Matching Logic - Extended Abstract (Invited Talk). RTA (2015)
Daejun Park, Andrei Stefanescu, Grigore Rosu
KJS: a complete formal semantics of JavaScript. PLDI (2015)
Philip Daian, Yliès Falcone, Patrick O'Neil Meredith, Traian-Florin Serbanuta, Shin'ichi Shiriashi, Akihito Iwai, Grigore Rosu
RV-Android: Efficient Parametric Android Runtime Verification, a Brief Tutorial. RV (2015)
Jeff Huang, Qingzhou Luo, Grigore Rosu
GPredict: Generic Predictive Concurrency Analysis. ICSE (1) (2015)
Andrei Popescu, Grigore Rosu
Term-generic logic. Theor. Comput. Sci. 577 (2015)
Grigore Rosu
From Rewriting Logic, to Programming Language Semantics, to Program Verification. Logic, Rewriting, and Concurrency (2015)
Denis Bogdanas, Grigore Rosu
K-Java: A Complete Semantics of Java. POPL (2015)
Owolabi Legunsen, Darko Marinov, Grigore Rosu
Evolution-Aware Monitoring-Oriented Programming. ICSE (2) (2015)
Stefan Ciobaca, Dorel Lucanu, Vlad Rusu, Grigore Rosu
A Language-Independent Proof System for Mutual Program Equivalence. ICFEM (2014)
Codruta Gîrlea, Grigore Rosu
Abstract Semantics for K Module Composition. Electron. Notes Theor. Comput. Sci. 304 (2014)
Traian-Florin Serbanuta, Andrei Arusoaie, David Lazar, Chucky Ellison, Dorel Lucanu, Grigore Rosu
The K Primer (version 3.3). Electron. Notes Theor. Comput. Sci. 304 (2014)
Jeff Huang, Patrick O'Neil Meredith, Grigore Rosu
Maximal sound predictive race detection with control flow abstraction. PLDI (2014)
Stefan Ciobaca, Dorel Lucanu, Vlad Rusu, Grigore Rosu
A Theoretical Foundation for Programming Languages Aggregation. WADT (2014)
Grigore Rosu, Dorel Lucanu
Behavioral Rewrite Systems and Behavioral Productivity. Specification, Algebra, and Software (2014)
Grigore Rosu, Traian-Florin Serbanuta
K Overview and SIMPLE Case Study. Electron. Notes Theor. Comput. Sci. 304 (2014)
Qingzhou Luo, Yi Zhang, Choonghwan Lee, Dongyun Jin, Patrick O'Neil Meredith, Traian-Florin Serbanuta, Grigore Rosu
RV-Monitor: Efficient Parametric Runtime Verification with Simultaneous Properties. RV (2014)
Jeff Huang, Cansu Erdogan, Yi Zhang, Brandon M. Moore, Qingzhou Luo, Aravind Sundaresan, Grigore Rosu
ROSRV: Runtime Verification for Robots. RV (2014)
Jörg Endrullis, Dimitri Hendriks, Rena Bakhshi, Grigore Rosu
On the complexity of stream equality. J. Funct. Program. 24 (2-3) (2014)
Andrei Arusoaie, Dorel Lucanu, Vlad Rusu, Traian-Florin Serbanuta, Andrei Stefanescu, Grigore Rosu
Language Definitions as Rewrite Theories. WRLA (2014)
Andrei Stefanescu, Stefan Ciobaca, Radu Mereuta, Brandon M. Moore, Traian-Florin Serbanuta, Grigore Rosu
All-Path Reachability Logic. RTA-TLCA (2014)
Grigore Rosu
Specifying Languages and Verifying Programs with K. SYNASC (2013)
Grigore Rosu, Andrei Stefanescu, Stefan Ciobaca, Brandon M. Moore
One-Path Reachability Logic. LICS (2013)
Patrick O'Neil Meredith, Grigore Rosu
Efficient parametric runtime verification with deterministic string rewriting. ASE (2013)
Qingzhou Luo, Grigore Rosu
EnforceMOP: a runtime property enforcement system for multithreaded programs. ISSTA (2013)
José Meseguer, Grigore Rosu
The rewriting logic semantics project: A progress report. Inf. Comput. 231 (2013)
Grigore Rosu, Feng Chen
Semantics and Algorithms for Parametric Monitoring Log. Methods Comput. Sci. 8 (1) (2012)
Soha Hussein, Patrick O'Neil Meredith, Grigore Rosu
Security-policy monitoring and enforcement with JavaMOP. PLAS (2012)
Traian-Florin Serbanuta, Feng Chen, Grigore Rosu
Maximal Causal Models for Sequentially Consistent Systems. RV (2012)
Oleg Sokolsky, Grigore Rosu
Introduction to the special issue on runtime verification. Formal Methods Syst. Des. 41 (3) (2012)
Grigore Rosu, Andrei Stefanescu
From Hoare Logic to Matching Logic Reachability. FM (2012)
David Lazar, Andrei Arusoaie, Traian-Florin Serbanuta, Chucky Ellison, Radu Mereuta, Dorel Lucanu, Grigore Rosu
Executing Formal Semantics with the K Tool. FM (2012)
Andrei Arusoaie, Traian-Florin Serbanuta, Chucky Ellison, Grigore Rosu
Making Maude Definitions More Interactive. WRLA (2012)
Dongyun Jin, Patrick O'Neil Meredith, Choonghwan Lee, Grigore Rosu
JavaMOP: Efficient parametric runtime monitoring framework. ICSE (2012)
Grigore Rosu, Andrei Stefanescu
Checking reachability using matching logic. OOPSLA (2012)
Chucky Ellison, Grigore Rosu
An executable formal semantics of C with applications. POPL (2012)
Dorel Lucanu, Traian-Florin Serbanuta, Grigore Rosu
K Framework Distilled. WRLA (2012)
Mark Hills, Feng Chen, Grigore Rosu
A Rewriting Logic Approach to Static Checking of Units of Measurement in C. Electron. Notes Theor. Comput. Sci. 290 (2012)
Traian-Florin Serbanuta, Grigore Rosu
A Truly Concurrent Semantics for the K Framework Based on Graph Transformations. ICGT (2012)
Grigore Rosu, Andrei Stefanescu
Towards a Unified Theory of Operational and Axiomatic Semantics. ICALP (2) (2012)
Patrick O'Neil Meredith, Dongyun Jin, Dennis Griffith, Feng Chen, Grigore Rosu
An overview of the MOP runtime verification framework. Int. J. Softw. Tools Technol. Transf. 14 (3) (2012)
Grigore Rosu
On Safety Properties and Their Monitoring. Sci. Ann. Comput. Sci. 22 (2) (2012)
Choonghwan Lee, Feng Chen, Grigore Rosu
Mining parametric specifications. ICSE (2011)
Grigore Rosu, Andrei Stefanescu
Matching logic: a new program verification approach. ICSE (2011)
José Meseguer, Grigore Rosu
The Rewriting Logic Semantics Project: A Progress Report. FCT (2011)
Vilas Jagannath, Milos Gligoric, Dongyun Jin, Qingzhou Luo, Grigore Rosu, Darko Marinov
Improved multithreaded unit testing. SIGSOFT FSE (2011)
Dongyun Jin, Patrick O'Neil Meredith, Dennis Griffith, Grigore Rosu
Garbage collection for monitoring parametric properties. PLDI (2011)
Eugen-Ioan Goriac, Dorel Lucanu, Grigore Rosu
Automating Coinduction with Case Analysis. ICFEM (2010)
Patrick O'Neil Meredith, Dongyun Jin, Feng Chen, Grigore Rosu
Efficient monitoring of parametric context-free patterns. Autom. Softw. Eng. 17 (2) (2010)
Patrick O'Neil Meredith, Michael Katelman, José Meseguer, Grigore Rosu
A formal executable semantics of Verilog. MEMOCODE (2010)
Mark Hills, Grigore Rosu
A Rewriting Logic Semantics Approach to Modular Program Analysis. RTA (2010)

Grigore Rosu.css-eqlu8i{font-size:small;padding-left:4px;}

Publication Activity (10 Years)

Top Topics

Top Venues

Grigore Rosu