Grigore Rosu - RankMe

235 papers A* 34A 17B 32C 5Misc 1Journal 51Unranked 83

Year	Rank	Type	Title / Venue / Authors
2026	B	`conf`	$\mathbb {K}$ Definitions as Matching Logic Theories, Formally. FoSSaCS Xiaohong Chen, Horatiu Cheval, Dorel Lucanu, Grigore Rosu
2026	—	`conf`	Actors and Blockchains, Together. Concurrent Programming, Open Systems and Formal Methods Xiaohong Chen, Grigore Rosu
2025	J	`jnl`	FastSet: Parallel Claim Settlement. CoRR Xiaohong Chen, Grigore Rosu
2024	—	`conf`	A Logical Treatment of Finite Automata. TACAS (1) Nishant Rodrigues, Mircea Sebe, Xiaohong Chen, Grigore Rosu
2023	J	`jnl`	Capturing constrained constructor patterns in matching logic. J. Log. Algebraic Methods Program. Xiaohong Chen, Dorel Lucanu, Grigore Rosu
2023	J	`jnl`	Generating Proof Certificates for a Language-Agnostic Deductive Program Verifier. Proc. ACM Program. Lang. Zhengyao Lin, Xiaohong Chen, Minh-Thai Trinh, John Wang, Grigore Rosu
2022	—	`ed.`	Model Checking Software - 28th International Symposium, SPIN 2022, Virtual Event, May 21, 2022, Proceedings SPIN Owolabi Legunsen, Grigore Rosu
2022	—	`ed.`	Tools and Algorithms for the Construction and Analysis of Systems - 28th International Conference, TACAS 2022, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Munich, Germany, April 2-7, 2022, Proceedings, Part I TACAS (1) Dana Fisman, Grigore Rosu
2022	—	`ed.`	Tools and Algorithms for the Construction and Analysis of Systems - 28th International Conference, TACAS 2022, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Munich, Germany, April 2-7, 2022, Proceedings, Part II TACAS (2) Dana Fisman, Grigore Rosu
2021	A*	`conf`	Language-parametric compiler validation with application to LLVM. ASPLOS Theodoros Kasampalis, Daejun Park, Zhengyao Lin, Vikram S. Adve, Grigore Rosu
2021	J	`jnl`	Matching logic explained. J. Log. Algebraic Methods Program. Xiaohong Chen, Dorel Lucanu, Grigore Rosu
2021	J	`jnl`	Rigorous Methods for Smart Contracts (Dagstuhl Seminar 21431). Dagstuhl Reports Nikolaj S. Bjørner, Maria Christakis, Matteo Maffei, Grigore Rosu
2021	—	`conf`	The K Vision for the Future of Programming Language Design and Analysis. Formal Methods in Outer Space Xiaohong Chen, Grigore Rosu
2021	—	`conf`	Towards a Trustworthy Semantics-Based Language Framework via Proof Generation. CAV (2) Xiaohong Chen, Zhengyao Lin, Minh-Thai Trinh, Grigore Rosu
2020	J	`jnl`	A general approach to define binders using matching logic. Proc. ACM Program. Lang. Xiaohong Chen, Grigore Rosu
2020	—	`conf`	Connecting Constrained Constructor Patterns and Matching Logic. WRLA Xiaohong Chen, Dorel Lucanu, Grigore Rosu
2020	—	`conf`	End-to-End Formal Verification of Ethereum 2.0 Deposit Smart Contract. CAV (1) Daejun Park, Yi Zhang, Grigore Rosu
2020	—	`conf`	Formal Design, Implementation and Verification of Blockchain Languages Using K (Invited Talk). FMBC@CAV Grigore Rosu
2020	—	`conf`	Formalizing Correct-by-Construction Casper in Coq. IEEE ICBC Elaine Li, Traian Serbanuta, Denisa Diaconescu, Vlad Zamfir, Grigore Rosu
2020	B	`conf`	Matching logic: the foundation of the K framework (invited talk). CPP Grigore Rosu, Xiaohong Chen
2020	J	`jnl`	Specification of the Giskard Consensus Protocol. CoRR Elaine Li, Karl Palmskog, Mircea Sebe, Grigore Rosu
2020	J	`jnl`	Towards a unified proof framework for automated fixpoint reasoning using matching logic. Proc. ACM Program. Lang. Xiaohong Chen, Minh-Thai Trinh, Nishant Rodrigues, Lucas Peña, Grigore Rosu
2019	—	`conf`	$\mathbb {K}$ - A Semantic Framework for Programming Languages and Formal Analysis. SETSS Xiaohong Chen, Grigore Rosu
2019	A*	`conf`	A complete formal semantics of x86-64 user-level instruction set architecture. PLDI Sandeep Dasgupta, Daejun Park, Theodoros Kasampalis, Vikram S. Adve, Grigore Rosu
2019	J	`jnl`	All-Path Reachability Logic. Log. Methods Comput. Sci. Andrei Stefanescu, Stefan Ciobaca, Radu Mereuta, Brandon M. Moore, Traian-Florin Serbanuta, Grigore Rosu
2019	J	`jnl`	Dealing With C's Original Sin. IEEE Softw. Chris Hathhorn, Grigore Rosu
2019	J	`jnl`	First international Competition on Runtime Verification: rules, benchmarks, tools, and final results of CRV 2014. Int. J. Softw. Tools Technol. Transf. 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
2019	J	`jnl`	How effective are existing Java API specifications for finding bugs during runtime verification? Autom. Softw. Eng. Owolabi Legunsen, Nader Al Awar, Xinyue Xu, Wajih Ul Hassan, Grigore Rosu, Darko Marinov
2019	B	`conf`	IELE: A Rigorously Designed Language and Tool Ecosystem for the Blockchain. FM Theodoros Kasampalis, Dwight Guth, Brandon M. Moore, Traian-Florin Serbanuta, Yi Zhang, Daniele Filaretti, Virgil Nicolae Serbanuta, Ralph Johnson, Grigore Rosu
2019	B	`conf`	Matching mu-Logic: Foundation of K Framework (Invited Paper). CALCO Xiaohong Chen, Grigore Rosu
2019	A*	`conf`	Matching μ-Logic. LICS Xiaohong Chen, Grigore Rosu
2019	—	`ch.`	Runtime Verification Past Experiences and Future Projections. Computing and Software Science Klaus Havelund, Giles Reger, Grigore Rosu
2019	—	`conf`	Statistical Model Checking of RANDAO's Resilience to Pre-computed Reveal Strategies. FM Workshops (1) Musab A. Alturki, Grigore Rosu
2019	A	`conf`	Techniques for Evolution-Aware Runtime Verification. ICST Owolabi Legunsen, Yi Zhang, Milica Hadzi-Tanovic, Grigore Rosu, Darko Marinov
2019	—	`conf`	Towards a Verified Model of the Algorand Consensus Protocol in Coq. FM Workshops (1) Musab A. Alturki, Jing Chen, Victor Luchangco, Brandon M. Moore, Karl Palmskog, Lucas Peña, Grigore Rosu
2019	J	`jnl`	Towards a Verified Model of the Algorand Consensus Protocol in Coq. CoRR Musab A. Alturki, Jing Chen, Victor Luchangco, Brandon M. Moore, Karl Palmskog, Lucas Peña, Grigore Rosu
2018	—	`conf`	A Language-Independent Approach to Smart Contract Verification. ISoLA (4) Xiaohong Chen, Daejun Park, Grigore Rosu
2018	—	`conf`	A Language-Independent Program Verification Framework. ISoLA (2) Xiaohong Chen, Grigore Rosu
2018	—	`conf`	A formal verification tool for Ethereum VM bytecode. ESEC/SIGSOFT FSE Daejun Park, Yi Zhang, Manasvi Saxena, Philip Daian, Grigore Rosu
2018	J	`jnl`	All-Path Reachability Logic. CoRR Andrei Stefanescu, Stefan Ciobaca, Radu Mereuta, Brandon M. Moore, Traian-Florin Serbanuta, Grigore Rosu
2018	J	`jnl`	Finite-trace linear temporal logic: coinductive completeness. Formal Methods Syst. Des. Grigore Rosu
2018	B	`conf`	Formal Design, Implementation and Verification of Blockchain Languages (Invited Talk). FSCD Grigore Rosu
2018	A	`conf`	KEVM: A Complete Formal Semantics of the Ethereum Virtual Machine. CSF Everett Hildenbrandt, Manasvi Saxena, Nishant Rodrigues, Xiaoran Zhu, Philip Daian, Dwight Guth, Brandon M. Moore, Daejun Park, Yi Zhang, Andrei Stefanescu, Grigore Rosu
2018	J	`jnl`	P4K: A Formal Semantics of P4 and Applications. CoRR Ali Kheradmand, Grigore Rosu
2018	A	`conf`	Program Verification by Coinduction. ESOP Brandon M. Moore, Lucas Peña, Grigore Rosu
2018	B	`conf`	Runtime Verification - 17 Years Later. RV Klaus Havelund, Grigore Rosu
2017	J	`jnl`	Matching Logic. CoRR Grigore Rosu
2017	J	`jnl`	Matching Logic. Log. Methods Comput. Sci. Grigore Rosu
2017	A*	`ed.`	Proceedings of the 32nd IEEE/ACM International Conference on Automated Software Engineering, ASE 2017, Urbana, IL, USA, October 30 - November 03, 2017 ASE Grigore Rosu, Massimiliano Di Penta, Tien N. Nguyen
2017	—	`ch.`	𝕂: A Semantic Framework for Programming Languages and Formal Analysis Tools. Dependable Software Systems Engineering Grigore Rosu
2016	J	`jnl`	A language-independent proof system for full program equivalence. Formal Aspects Comput. Stefan Ciobaca, Dorel Lucanu, Vlad Rusu, Grigore Rosu
2016	B	`conf`	Finite-Trace Linear Temporal Logic: Coinductive Completeness. RV Grigore Rosu
2016	A*	`conf`	How good are the specs? a study of the bug-finding effectiveness of existing Java API specifications. ASE Owolabi Legunsen, Wajih Ul Hassan, Xinyue Xu, Grigore Rosu, Darko Marinov
2016	J	`jnl`	Language definitions as rewrite theories. J. Log. Algebraic Methods Program. Vlad Rusu, Dorel Lucanu, Traian-Florin Serbanuta, Andrei Arusoaie, Andrei Stefanescu, Grigore Rosu
2016	—	`conf`	RV-Match: Practical Semantics-Based Program Analysis. CAV (1) Dwight Guth, Chris Hathhorn, Manasvi Saxena, Grigore Rosu
2016	B	`conf`	Runtime Verification at Work: A Tutorial. RV Philip Daian, Dwight Guth, Chris Hathhorn, Yilong Li, Edgar Pek, Manasvi Saxena, Traian-Florin Serbanuta, Grigore Rosu
2016	A	`conf`	Semantics-based program verifiers for all languages. OOPSLA Andrei Stefanescu, Daejun Park, Shijiao Yuwen, Yilong Li, Grigore Rosu
2016	—	`conf`	Towards a \mathbb K K ool Future. Theory and Practice of Formal Methods Dorel Lucanu, Traian-Florin Serbanuta, Grigore Rosu
2015	A*	`conf`	Defining the undefinedness of C. PLDI Chris Hathhorn, Chucky Ellison, Grigore Rosu
2015	—	`conf`	Evolution-Aware Monitoring-Oriented Programming. ICSE (2) Owolabi Legunsen, Darko Marinov, Grigore Rosu
2015	—	`conf`	From Rewriting Logic, to Programming Language Semantics, to Program Verification. Logic, Rewriting, and Concurrency Grigore Rosu
2015	—	`conf`	GPredict: Generic Predictive Concurrency Analysis. ICSE (1) Jeff Huang, Qingzhou Luo, Grigore Rosu
2015	A*	`conf`	K-Java: A Complete Semantics of Java. POPL Denis Bogdanas, Grigore Rosu
2015	A*	`conf`	KJS: a complete formal semantics of JavaScript. PLDI Daejun Park, Andrei Stefanescu, Grigore Rosu
2015	—	`conf`	Matching Logic - Extended Abstract (Invited Talk). RTA Grigore Rosu
2015	B	`conf`	RV-Android: Efficient Parametric Android Runtime Verification, a Brief Tutorial. RV Philip Daian, Yliès Falcone, Patrick O'Neil Meredith, Traian-Florin Serbanuta, Shinichi Shiraishi, Akihito Iwai, Grigore Rosu
2015	J	`jnl`	Term-generic logic. Theor. Comput. Sci. Andrei Popescu, Grigore Rosu
2014	C	`conf`	A Language-Independent Proof System for Mutual Program Equivalence. ICFEM Stefan Ciobaca, Dorel Lucanu, Vlad Rusu, Grigore Rosu
2014	—	`conf`	A Theoretical Foundation for Programming Languages Aggregation. WADT Stefan Ciobaca, Dorel Lucanu, Vlad Rusu, Grigore Rosu
2014	—	`conf`	All-Path Reachability Logic. RTA-TLCA Andrei Stefanescu, Stefan Ciobaca, Radu Mereuta, Brandon M. Moore, Traian-Florin Serbanuta, Grigore Rosu
2014	—	`conf`	Behavioral Rewrite Systems and Behavioral Productivity. Specification, Algebra, and Software Grigore Rosu, Dorel Lucanu
2014	—	`conf`	Language Definitions as Rewrite Theories. WRLA Andrei Arusoaie, Dorel Lucanu, Vlad Rusu, Traian-Florin Serbanuta, Andrei Stefanescu, Grigore Rosu
2014	A*	`conf`	Maximal sound predictive race detection with control flow abstraction. PLDI Jeff Huang, Patrick O'Neil Meredith, Grigore Rosu
2014	J	`jnl`	On the complexity of stream equality. J. Funct. Program. Jörg Endrullis, Dimitri Hendriks, Rena Bakhshi, Grigore Rosu
2014	B	`conf`	ROSRV: Runtime Verification for Robots. RV Jeff Huang, Cansu Erdogan, Yi Zhang, Brandon M. Moore, Qingzhou Luo, Aravind Sundaresan, Grigore Rosu
2014	B	`conf`	RV-Monitor: Efficient Parametric Runtime Verification with Simultaneous Properties. RV Qingzhou Luo, Yi Zhang, Choonghwan Lee, Dongyun Jin, Patrick O'Neil Meredith, Traian-Florin Serbanuta, Grigore Rosu
2013	A*	`conf`	Efficient parametric runtime verification with deterministic string rewriting. ASE Patrick O'Neil Meredith, Grigore Rosu
2013	A	`conf`	EnforceMOP: a runtime property enforcement system for multithreaded programs. ISSTA Qingzhou Luo, Grigore Rosu
2013	A*	`conf`	One-Path Reachability Logic. LICS Grigore Rosu, Andrei Stefanescu, Stefan Ciobaca, Brandon M. Moore
2013	Misc	`conf`	Specifying Languages and Verifying Programs with K. SYNASC Grigore Rosu
2013	J	`jnl`	The rewriting logic semantics project: A progress report. Inf. Comput. José Meseguer, Grigore Rosu
2012	B	`conf`	A Truly Concurrent Semantics for the K Framework Based on Graph Transformations. ICGT Traian-Florin Serbanuta, Grigore Rosu
2012	A*	`conf`	An executable formal semantics of C with applications. POPL Chucky Ellison, Grigore Rosu
2012	J	`jnl`	An overview of the MOP runtime verification framework. Int. J. Softw. Tools Technol. Transf. Patrick O'Neil Meredith, Dongyun Jin, Dennis Griffith, Feng Chen, Grigore Rosu
2012	A	`conf`	Checking reachability using matching logic. OOPSLA Grigore Rosu, Andrei Stefanescu
2012	B	`conf`	Executing Formal Semantics with the K Tool. FM David Lazar, Andrei Arusoaie, Traian-Florin Serbanuta, Chucky Ellison, Radu Mereuta, Dorel Lucanu, Grigore Rosu
2012	—	`ed.`	Formal Techniques for Distributed Systems - Joint 14th IFIP WG 6.1 International Conference, FMOODS 2012 and 32nd IFIP WG 6.1 International Conference, FORTE 2012, Stockholm, Sweden, June 13-16, 2012. Proceedings FMOODS/FORTE Holger Giese, Grigore Rosu
2012	B	`conf`	From Hoare Logic to Matching Logic Reachability. FM Grigore Rosu, Andrei Stefanescu
2012	J	`jnl`	Introduction to the special issue on runtime verification. Formal Methods Syst. Des. Oleg Sokolsky, Grigore Rosu
2012	A*	`conf`	JavaMOP: Efficient parametric runtime monitoring framework. ICSE Dongyun Jin, Patrick O'Neil Meredith, Choonghwan Lee, Grigore Rosu
2012	—	`conf`	K Framework Distilled. WRLA Dorel Lucanu, Traian-Florin Serbanuta, Grigore Rosu
2012	—	`conf`	Making Maude Definitions More Interactive. WRLA Andrei Arusoaie, Traian-Florin Serbanuta, Chucky Ellison, Grigore Rosu
2012	B	`conf`	Maximal Causal Models for Sequentially Consistent Systems. RV Traian-Florin Serbanuta, Feng Chen, Grigore Rosu
2012	J	`jnl`	On Safety Properties and Their Monitoring. Sci. Ann. Comput. Sci. Grigore Rosu
2012	—	`conf`	Security-policy monitoring and enforcement with JavaMOP. PLAS Soha Hussein, Patrick O'Neil Meredith, Grigore Rosu
2012	J	`jnl`	Semantics and Algorithms for Parametric Monitoring Log. Methods Comput. Sci. Grigore Rosu, Feng Chen
2012	—	`conf`	Towards a Unified Theory of Operational and Axiomatic Semantics. ICALP (2) Grigore Rosu, Andrei Stefanescu
2011	—	`conf`	Abstract Semantics for K Module Composition. K Codruta Gîrlea, Grigore Rosu
2011	A*	`conf`	Garbage collection for monitoring parametric properties. PLDI Dongyun Jin, Patrick O'Neil Meredith, Dennis Griffith, Grigore Rosu
2011	—	`conf`	Improved multithreaded unit testing. SIGSOFT FSE Vilas Jagannath, Milos Gligoric, Dongyun Jin, Qingzhou Luo, Grigore Rosu, Darko Marinov
2011	—	`conf`	K Overview and SIMPLE Case Study. K Grigore Rosu, Traian-Florin Serbanuta
2011	A*	`conf`	Matching logic: a new program verification approach. ICSE Grigore Rosu, Andrei Stefanescu
2011	A*	`conf`	Mining parametric specifications. ICSE Choonghwan Lee, Feng Chen, Grigore Rosu
2011	—	`conf`	The K Primer (version 3.3). K Traian-Florin Serbanuta, Andrei Arusoaie, David Lazar, Chucky Ellison, Dorel Lucanu, Grigore Rosu
2011	B	`conf`	The Rewriting Logic Semantics Project: A Progress Report. FCT José Meseguer, Grigore Rosu
2010	—	`conf`	A Rewriting Logic Semantics Approach to Modular Program Analysis. RTA Mark Hills, Grigore Rosu
2010	C	`conf`	A formal executable semantics of Verilog. MEMOCODE Patrick O'Neil Meredith, Michael Katelman, José Meseguer, Grigore Rosu
2010	J	`jnl`	An overview of the K semantic framework. J. Log. Algebraic Methods Program. Grigore Rosu, Traian-Florin Serbanuta
2010	C	`conf`	Automating Coinduction with Case Analysis. ICFEM Eugen-Ioan Goriac, Dorel Lucanu, Grigore Rosu
2010	J	`jnl`	Efficient monitoring of parametric context-free patterns. Autom. Softw. Eng. Patrick O'Neil Meredith, Dongyun Jin, Feng Chen, Grigore Rosu
2010	—	`conf`	IMUnit: improved multithreaded unit testing. IWMSE@ICSE Vilas Jagannath, Milos Gligoric, Dongyun Jin, Grigore Rosu, Darko Marinov
2010	—	`conf`	K-Maude: A Rewriting Based Tool for Semantics of Programming Languages. WRLA Traian-Florin Serbanuta, Grigore Rosu
2010	—	`conf`	Matching Logic: An Alternative to Hoare/Floyd Logic. AMAST Grigore Rosu, Chucky Ellison, Wolfram Schulte
2010	B	`ed.`	Runtime Verification - First International Conference, RV 2010, St. Julians, Malta, November 1-4, 2010. Proceedings RV Howard Barringer, Yliès Falcone, Bernd Finkbeiner, Klaus Havelund, Insup Lee, Gordon J. Pace, Grigore Rosu, Oleg Sokolsky, Nikolai Tillmann
2010	B	`conf`	Runtime Verification with the RV System. RV Patrick O'Neil Meredith, Grigore Rosu
2009	J	`jnl`	A rewriting logic approach to operational semantics. Inf. Comput. Traian-Florin Serbanuta, Grigore Rosu, José Meseguer
2009	J	`jnl`	A semantic approach to interpolation. Theor. Comput. Sci. Andrei Popescu, Traian-Florin Serbanuta, Grigore Rosu
2009	B	`conf`	CIRC: A Behavioral Verification Tool Based on Circular Coinduction. CALCO Dorel Lucanu, Eugen-Ioan Goriac, Georgiana Caltais, Grigore Rosu
2009	C	`conf`	Circular Coinduction with Special Contexts. ICFEM Dorel Lucanu, Grigore Rosu
2009	B	`conf`	Circular Coinduction: A Proof Theoretical Foundation. CALCO Grigore Rosu, Dorel Lucanu
2009	—	`conf`	Dependent advice: a general approach to optimizing history-based aspects. AOSD Eric Bodden, Feng Chen, Grigore Rosu
2009	A*	`conf`	Efficient Formalism-Independent Monitoring of Parametric Properties. ASE Feng Chen, Patrick O'Neil Meredith, Dongyun Jin, Grigore Rosu
2009	A	`conf`	Parametric Trace Slicing and Monitoring. TACAS Feng Chen, Grigore Rosu
2009	—	`ed.`	Proceedings of the Seventh International Workshop on Rewriting Logic and its Applications, WRLA 2008, Budapest, Hungary, March 29-30, 2008 WRLA Grigore Rosu
2009	B	`conf`	Runtime Verification of C Memory Safety. RV Grigore Rosu, Wolfram Schulte, Traian-Florin Serbanuta
2008	—	`conf`	A Rewriting Logic Approach to Static Checking of Units of Measurement in C. RULE Mark Hills, Feng Chen, Grigore Rosu
2008	—	`conf`	A Rewriting Logic Approach to Type Inference. WADT Chucky Ellison, Traian-Florin Serbanuta, Grigore Rosu
2008	—	`ed.`	Algebraic Methodology and Software Technology, 12th International Conference, AMAST 2008, Urbana, IL, USA, July 28-31, 2008, Proceedings AMAST José Meseguer, Grigore Rosu
2008	—	`conf`	Defining and Executing P Systems with Structured Data in K. Workshop on Membrane Computing Traian Serbanuta, Gheorghe Stefanescu, Grigore Rosu
2008	A*	`conf`	Efficient Monitoring of Parametric Context-Free Patterns. ASE Patrick O'Neil Meredith, Dongyun Jin, Feng Chen, Grigore Rosu
2008	A	`conf`	Hardware Runtime Monitoring for Dependable COTS-Based Real-Time Embedded Systems. RTSS Rodolfo Pellizzoni, Patrick O'Neil Meredith, Marco Caccamo, Grigore Rosu
2008	—	`conf`	Preface. WRLA Grigore Rosu
2008	B	`ed.`	Runtime Verification, 02.01. - 06.01.2007 Runtime Verification Bernd Finkbeiner, Klaus Havelund, Grigore Rosu, Oleg Sokolsky
2008	B	`conf`	Synthesizing Monitors for Safety Properties: This Time with Calls and Returns. RV Grigore Rosu, Feng Chen, Thomas Ball
2008	—	`conf`	Term-Generic Logic. WADT Andrei Popescu, Grigore Rosu
2008	—	`conf`	Towards a Module System for K. WADT Mark Hills, Grigore Rosu
2008	A*	`conf`	jPredictor: a predictive runtime analysis tool for java. ICSE Feng Chen, Traian-Florin Serbanuta, Grigore Rosu
2007	B	`conf`	07011 Abstracts Collection -- Runtime Verification. Runtime Verification Bernd Finkbeiner, Klaus Havelund, Grigore Rosu, Oleg Sokolsky
2007	B	`conf`	07011 Executive Summary -- Runtime Verification. Runtime Verification Bernd Finkbeiner, Klaus Havelund, Grigore Rosu, Oleg Sokolsky
2007	—	`conf`	A Rewriting Logic Approach to Operational Semantics (Extended Abstract). SOS@LICS/ICALP Traian-Florin Serbanuta, Grigore Rosu, José Meseguer
2007	—	`conf`	A rewriting approach to the design and evolution of object-oriented languages. OOPSLA Companion Mark Hills, Grigore Rosu
2007	B	`conf`	An Effective Algorithm for the Membership Problem for Extended Regular Expressions. FoSSaCS Grigore Rosu
2007	J	`jnl`	An instrumentation technique for online analysis of multithreaded programs. Concurr. Comput. Pract. Exp. Grigore Rosu, Koushik Sen
2007	B	`conf`	CIRC : A Circular Coinductive Prover. CALCO Dorel Lucanu, Grigore Rosu
2007	J	`jnl`	Editorial. High. Order Symb. Comput. Narciso Martí-Oliet, Grigore Rosu, Carolyn L. Talcott
2007	—	`conf`	KOOL: An Application of Rewriting Logic to Language Prototyping and Analysis. RTA Mark Hills, Grigore Rosu
2007	A	`conf`	Mop: an efficient and generic runtime verification framework. OOPSLA Feng Chen, Grigore Rosu
2007	—	`conf`	On Formal Analysis of OO Languages Using Rewriting Logic: Designing for Performance. FMOODS Mark Hills, Grigore Rosu
2007	A*	`conf`	Parametric and Sliced Causality. CAV Feng Chen, Grigore Rosu
2007	—	`conf`	Regular Strategies as Proof Tactics for CIRC. WRS@RDP Dorel Lucanu, Grigore Rosu, Gheorghe Grigoras
2007	J	`jnl`	The rewriting logic semantics project. Theor. Comput. Sci. José Meseguer, Grigore Rosu
2006	—	`conf`	A Rewrite Framework for Language Definitions and for Generation of Efficient Interpreters. WRLA Mark Hills, Traian Serbanuta, Grigore Rosu
2006	B	`conf`	A Semantic Approach to Interpolation. FoSSaCS Andrei Popescu, Traian Serbanuta, Grigore Rosu
2006	A*	`conf`	Allen Linear (Interval) Temporal Logic - Translation to LTL and Monitor Synthesis. CAV Grigore Rosu, Saddek Bensalem
2006	—	`conf`	Complete Categorical Deduction for Satisfaction as Injectivity. Essays Dedicated to Joseph A. Goguen Grigore Rosu
2006	—	`conf`	Computationally Equivalent Elimination of Conditions. RTA Traian-Florin Serbanuta, Grigore Rosu
2006	A	`conf`	Decentralized runtime analysis of multithreaded applications. IPDPS Koushik Sen, Abhay Vardhan, Gul Agha, Grigore Rosu
2006	A	`conf`	Equality of streams is a Pi0 over 2-complete problem. ICFP Grigore Rosu
2006	—	`ed.`	Formal Approaches to Software Testing and Runtime Verification, First Combined International Workshops, FATES 2006 and RV 2006, Seattle, WA, USA, August 15-16, 2006, Revised Selected Papers FATES/RV Klaus Havelund, Manuel Núñez, Grigore Rosu, Burkhart Wolff
2006	J	`jnl`	Online efficient predictive safety analysis of multithreaded programs. Int. J. Softw. Tools Technol. Transf. Koushik Sen, Grigore Rosu, Gul Agha
2006	B	`conf`	Parametric and Termination-Sensitive Control Dependence. SAS Feng Chen, Grigore Rosu
2006	—	`conf`	Rewriting Logic Systems. WRLA Grit Denker, Carolyn L. Talcott, Grigore Rosu, Mark van den Brand, Steven Eker, Traian-Florin Serbanuta
2006	A	`conf`	Static Analysis to Enforce Safe Value Flow in Embedded Control Systems. DSN Sumant Kowshik, Grigore Rosu, Lui Sha
2005	A*	`conf`	A Tree Based Router Search Engine Architecture with Single Port Memories. ISCA Florin Baboescu, Dean M. Tullsen, Grigore Rosu, Sumeet Singh
2005	J	`jnl`	An Equational Specification for the Scheme Language. J. Univers. Comput. Sci. Marcelo d'Amorim, Grigore Rosu
2005	B	`conf`	Behavioral Extensions of Institutions. CALCO Andrei Popescu, Grigore Rosu
2005	—	`conf`	Checking and Correcting Behaviors of Java Programs at Runtime with Java-MOP. RV@CAV Feng Chen, Marcelo d'Amorim, Grigore Rosu
2005	J	`jnl`	Combining test case generation and runtime verification. Theor. Comput. Sci. Cyrille Artho, Howard Barringer, Allen Goldberg, Klaus Havelund, Sarfraz Khurshid, Michael R. Lowry, Corina S. Pasareanu, Grigore Rosu, Koushik Sen, Willem Visser, Richard Washington
2005	—	`conf`	Computational Logical Frameworks and Generic Program Analysis Technologies. VSTTE José Meseguer, Grigore Rosu
2005	—	`conf`	Detecting Errors in Multithreaded Programs by Generalized Predictive Analysis of Executions. FMOODS Koushik Sen, Grigore Rosu, Gul Agha
2005	A*	`conf`	Efficient Monitoring of omega-Languages. CAV Marcelo d'Amorim, Grigore Rosu
2005	J	`jnl`	Foreword. Formal Methods Syst. Des. Klaus Havelund, Grigore Rosu
2005	B	`conf`	Formally Defining and Verifying Master/Slave Speculative Parallelization. FM Pierre Salverda, Grigore Rosu, Craig B. Zilles
2005	A	`conf`	Java-MOP: A Monitoring Oriented Programming Environment for Java. TACAS Feng Chen, Grigore Rosu
2005	—	`ed.`	Proceedings of the Fourth Workshop on Runtime Verification, RV@ETAPS 2004, Barcelona, Spain, April 3, 2004 RV@ETAPS Klaus Havelund, Grigore Rosu
2005	J	`jnl`	Rewriting-Based Techniques for Runtime Verification. Autom. Softw. Eng. Grigore Rosu, Klaus Havelund
2005	—	`conf`	The Rewriting Logic Semantics Project. SOS@ICALP José Meseguer, Grigore Rosu
2004	C	`conf`	A Formal Monitoring-Based Framework for Software Development and Analysis. ICFEM Feng Chen, Marcelo d'Amorim, Grigore Rosu
2004	A	`conf`	An Instrumentation Technique for Online Analysis of Multithreaded Programs. IPDPS Grigore Rosu, Koushik Sen
2004	J	`jnl`	An Overview of the Runtime Verification Tool Java PathExplorer. Formal Methods Syst. Des. Klaus Havelund, Grigore Rosu
2004	J	`jnl`	Behavioral abstraction is hiding information. Theor. Comput. Sci. Grigore Rosu
2004	—	`conf`	Composing Hidden Information Modules over Inclusive Institutions. Essays in Memory of Ole-Johan Dahl Joseph A. Goguen, Grigore Rosu
2004	A*	`conf`	Efficient Decentralized Monitoring of Safety in Distributed Systems. ICSE Koushik Sen, Abhay Vardhan, Gul Agha, Grigore Rosu
2004	J	`jnl`	Efficient monitoring of safety properties. Int. J. Softw. Tools Technol. Transf. Klaus Havelund, Grigore Rosu
2004	A*	`conf`	Extensional Theories and Rewriting. ICALP Grigore Rosu
2004	J	`jnl`	Foreword - Selected Papers from the First International Workshop on Runtime Verification held in Paris, July 2001 (RV'01). Formal Methods Syst. Des. Klaus Havelund, Grigore Rosu
2004	A*	`conf`	Formal Analysis of Java Programs in JavaFAN. CAV Azadeh Farzan, Feng Chen, José Meseguer, Grigore Rosu
2004	—	`conf`	Formal JVM Code Analysis in JavaFAN. AMAST Azadeh Farzan, José Meseguer, Grigore Rosu
2004	—	`conf`	From Conditional to Unconditional Rewriting. WADT Grigore Rosu
2004	—	`conf`	Monitoring Algorithms for Metric Temporal Logic Specifications. RV@ETAPS Prasanna Thati, Grigore Rosu
2004	A	`conf`	Online Efficient Predictive Safety Analysis of Multithreaded Programs. TACAS Koushik Sen, Grigore Rosu, Gul Agha
2004	—	`conf`	Preface. RV@ETAPS Klaus Havelund, Grigore Rosu
2004	A	`conf`	Rewriting Logic Semantics: From Language Specifications to Formal Analysis Tools. IJCAR José Meseguer, Grigore Rosu
2003	A*	`conf`	Certifying Measurement Unit Safety Polic. ASE Grigore Rosu, Feng Chen
2003	A*	`conf`	Certifying Optimality of State Estimation Programs. CAV Grigore Rosu, Ram Prasad Venkatesan, Jon Whittle, Laurentiu Leustean
2003	—	`conf`	Certifying and Synthesizing Membership Equational Proofs. FME Grigore Rosu, Steven Eker, Patrick Lincoln, José Meseguer
2003	—	`conf`	Experiments with Test Case Generation and Runtime Analysis. Abstract State Machines Cyrille Artho, Doron Drusinsky, Allen Goldberg, Klaus Havelund, Michael R. Lowry, Corina S. Pasareanu, Grigore Rosu, Willem Visser
2003	—	`conf`	Generating Optimal Linear Temporal Logic Monitors by Coinduction. ASIAN Koushik Sen, Grigore Rosu, Gul Agha
2003	—	`conf`	Generating Optimal Monitors for Extended Regular Expressions. RV@CAV Koushik Sen, Grigore Rosu
2003	—	`conf`	Inductive Behavioral Proofs by Unhiding. CMCS Grigore Rosu
2003	—	`conf`	Rule-Based Analysis of Dimensional Safety. RTA Feng Chen, Grigore Rosu, Ram Prasad Venkatesan
2003	—	`conf`	Runtime safety analysis of multithreaded programs. ESEC / SIGSOFT FSE Koushik Sen, Grigore Rosu, Gul Agha
2003	—	`conf`	Testing Extended Regular Language Membership Incrementally by Rewriting. RTA Grigore Rosu, Mahesh Viswanathan
2003	—	`conf`	Towards Monitoring-Oriented Programming: A Paradigm Combining Specification and Implementation. RV@CAV Feng Chen, Grigore Rosu
2002	A*	`conf`	A Total Approach to Partial Algebraic Specification. ICALP José Meseguer, Grigore Rosu
2002	J	`jnl`	Axiomatizability in Inclusive Equational Logics. Math. Struct. Comput. Sci. Grigore Rosu
2002	—	`conf`	Conditional Circular Coinductive Rewriting with Case Analysis. WADT Joseph A. Goguen, Kai Lin, Grigore Rosu
2002	J	`jnl`	Institution Morphisms. Formal Aspects Comput. Joseph A. Goguen, Grigore Rosu
2002	—	`conf`	On implementing behavioral rewriting. ACM SIGPLAN Workshop on Rule-Based Programming Grigore Rosu
2002	—	`conf`	Preface. RV@FLoC Klaus Havelund, Grigore Rosu
2002	—	`ed.`	Runtime Verification 2002, RV 2002, FLoC Satellite Event, Copenhagen, Denmark, July 26, 2002 RV@FLoC Klaus Havelund, Grigore Rosu
2002	A	`conf`	Synthesizing Monitors for Safety Properties. TACAS Klaus Havelund, Grigore Rosu
2002	—	`conf`	Towards Behavioral Maude: Behavioral Membership Equational Logic. CMCS José Meseguer, Grigore Rosu
2002	A*	`conf`	Towards Certifying Domain-Specific Properties of Synthesized Code. ASE Grigore Rosu, Jon Whittle
2001	A*	`conf`	Certifying Domain-Specific Policies. ASE Michael R. Lowry, Thomas Pressburger, Grigore Rosu
2001	B	`conf`	Complete Categorical Equational Deduction. CSL Grigore Rosu
2001	J	`jnl`	Equational axiomatizability for coalgebra. Theor. Comput. Sci. Grigore Rosu
2001	—	`conf`	Interpreting Abstract Interpretations in Membership Equational Logic. RULE@PLI Bernd Fischer, Grigore Rosu
2001	—	`conf`	Monitoring Java Programs with Java PathExplorer. RV@CAV Klaus Havelund, Grigore Rosu
2001	A*	`conf`	Monitoring Programs Using Rewriting. ASE Klaus Havelund, Grigore Rosu
2001	—	`conf`	Preface. RV@CAV Klaus Havelund, Grigore Rosu
2001	—	`ed.`	Workshop on Runtime Verification, RV 2001, in connection with CAV 2001, Paris, France, July 23, 2001 RV@CAV Klaus Havelund, Grigore Rosu
2000	—	`conf`	Behavioral and Coinductive Rewriting. WRLA Joseph A. Goguen, Kai Lin, Grigore Rosu
2000	A*	`conf`	Circular Coinductive Rewriting. ASE Joseph A. Goguen, Kai Lin, Grigore Rosu
2000	—	`conf`	Incompleteness of Behavioral Logics. CMCS Samuel R. Buss, Grigore Rosu
2000	J	`jnl`	On Equational Craig Interpolation. J. Univers. Comput. Sci. Grigore Rosu, Joseph A. Goguen
2000	J	`jnl`	Weak Inclusion Systems: Part Two. J. Univers. Comput. Sci. Virgil Emil Cazanescu, Grigore Rosu
1999	—	`conf`	A protocol for distributed cooperative work. WDS@FCT Joseph A. Goguen, Grigore Rosu
1999	—	`conf`	Hiding More of Hidden Algebra. World Congress on Formal Methods Joseph A. Goguen, Grigore Rosu
1999	J	`jnl`	Kan Extensions of Institutions. J. Univers. Comput. Sci. Grigore Rosu
1998	—	`conf`	A Birkhoff-like Axiomatizability Result for Hidden Algebra and Coalgebra. CMCS Grigore Rosu
1998	—	`conf`	Hidden Congruent Deduction. FTP (LNCS Selection) Grigore Rosu, Joseph A. Goguen
1997	A*	`conf`	Distributed Cooperative Formal Methods Tools. ASE Joseph A. Goguen, Kai Lin, Akira Mori, Grigore Rosu, Akiyoshi Sato
1997	J	`jnl`	Weak Inclusion Systems. Math. Struct. Comput. Sci. Virgil Emil Cazanescu, Grigore Rosu
1994	J	`jnl`	The Institution of Order-Sorted Equational Logic. Bull. EATCS Grigore Rosu