default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCIDGrigore Rosu
Person information
- affiliation: University of Illinois, Urbana-Champaign, IL, USA
Refine list
refinements active!
zoomed in on ?? of ?? records
view refined list in
export refined list as
showing all ?? records
2020 – today
- 2024
[c165]Nishant Rodrigues
, Mircea Sebe, Xiaohong Chen, Grigore Rosu:
A Logical Treatment of Finite Automata. TACAS (1) 2024: 350-369- 2023
- [j44]Xiaohong Chen, Dorel Lucanu, Grigore Rosu:
Capturing constrained constructor patterns in matching logic. J. Log. Algebraic Methods Program. 130: 100810 (2023) - [j43]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): 56-84 (2023) - 2022
- [e13]Owolabi Legunsen, Grigore Rosu:
Model Checking Software - 28th International Symposium, SPIN 2022, Virtual Event, May 21, 2022, Proceedings. Lecture Notes in Computer Science 13255, Springer 2022, ISBN 978-3-031-15076-0 [contents] - [e12]Dana Fisman, Grigore Rosu:
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. Lecture Notes in Computer Science 13243, Springer 2022, ISBN 978-3-030-99523-2 [contents] - [e11]Dana Fisman, Grigore Rosu:
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. Lecture Notes in Computer Science 13244, Springer 2022, ISBN 978-3-030-99526-3 [contents] - [d7]Zhengyao Lin, Xiaohong Chen, Minh-Thai Trinh, John Wang, Grigore Rosu:
Generating Proof Certificates for a Language-Agnostic Deductive Program Verifier. Zenodo, 2022
- [d6]Zhengyao Lin, Xiaohong Chen, Minh-Thai Trinh, John Wang, Grigore Rosu:
Generating Proof Certificates for a Language-Agnostic Deductive Program Verifier. Zenodo, 2022 - [d5]Zhengyao Lin, Xiaohong Chen, Minh-Thai Trinh, John Wang, Grigore Rosu:
Generating Proof Certificates for a Language-Agnostic Deductive Program Verifier. Zenodo, 2022 - [d4]Zhengyao Lin, Xiaohong Chen, Minh-Thai Trinh, John Wang, Grigore Rosu:
Generating Proof Certificates for a Language-Agnostic Deductive Program Verifier. Zenodo, 2022 - 2021
- [j42]Xiaohong Chen, Dorel Lucanu, Grigore Rosu:
Matching logic explained. J. Log. Algebraic Methods Program. 120: 100638 (2021) - [c164]Theodoros Kasampalis, Daejun Park, Zhengyao Lin, Vikram S. Adve, Grigore Rosu:
Language-parametric compiler validation with application to LLVM. ASPLOS 2021: 1004-1019 - [c163]Xiaohong Chen, Grigore Rosu:
The K Vision for the Future of Programming Language Design and Analysis. Formal Methods in Outer Space 2021: 3-9 - [c162]Xiaohong Chen, Zhengyao Lin, Minh-Thai Trinh, Grigore Rosu:
Towards a Trustworthy Semantics-Based Language Framework via Proof Generation. CAV (2) 2021: 477-499 - [d3]Xiaohong Chen, Zhengyao Lin, Minh-Thai Trinh, Grigore Rosu:
Towards a Trustworthy Semantics-Based Language Framework via Proof Generation. Zenodo, 2021 - [d2]Xiaohong Chen, Zhengyao Lin, Minh-Thai Trinh, Grigore Rosu:
Towards a Trustworthy Semantics-Based Language Framework via Proof Generation. Zenodo, 2021 - [d1]Xiaohong Chen, Zhengyao Lin, Minh-Thai Trinh, Grigore Rosu:
Towards a Trustworthy Semantics-Based Language Framework via Proof Generation. Zenodo, 2021 - [i8]Nikolaj S. Bjørner, Maria Christakis, Matteo Maffei, Grigore Rosu:
Rigorous Methods for Smart Contracts (Dagstuhl Seminar 21431). Dagstuhl Reports 11(9): 80-101 (2021) - 2020
- [j41]Xiaohong Chen, Grigore Rosu:
A general approach to define binders using matching logic. Proc. ACM Program. Lang. 4(ICFP): 88:1-88:32 (2020) - [j40]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): 161:1-161:29 (2020) - [c161]Grigore Rosu:
Formal Design, Implementation and Verification of Blockchain Languages Using K (Invited Talk). FMBC@CAV 2020: 1:1-1:1 - [c160]Daejun Park, Yi Zhang, Grigore Rosu:
End-to-End Formal Verification of Ethereum 2.0 Deposit Smart Contract. CAV (1) 2020: 151-164 - [c159]Grigore Rosu, Xiaohong Chen:
Matching logic: the foundation of the K framework (invited talk). CPP 2020: 1 - [c158]Elaine Li, Traian Serbanuta, Denisa Diaconescu, Vlad Zamfir, Grigore Rosu:
Formalizing Correct-by-Construction Casper in Coq. IEEE ICBC 2020: 1-3 - [c157]Xiaohong Chen, Dorel Lucanu, Grigore Rosu:
Connecting Constrained Constructor Patterns and Matching Logic. WRLA@ETAPS 2020: 19-37 - [i7]Elaine Li, Karl Palmskog, Mircea Sebe, Grigore Rosu:
Specification of the Giskard Consensus Protocol. CoRR abs/2010.02124 (2020)
2010 – 2019
- 2019
- [j39]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): 795-837 (2019) - [j38]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) - [j37]Chris Hathhorn, Grigore Rosu:
Dealing With C's Original Sin. IEEE Softw. 36(5): 24-28 (2019) - [j36]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): 31-70 (2019) - [c156]Xiaohong Chen, Grigore Rosu:
Matching mu-Logic: Foundation of K Framework (Invited Paper). CALCO 2019: 1:1-1:4 - [c155]Musab A. Alturki, Grigore Rosu:
Statistical Model Checking of RANDAO's Resilience to Pre-computed Reveal Strategies. FM Workshops (1) 2019: 337-349 - [c154]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: 362-367 - [c153]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: 593-610 - [c152]Owolabi Legunsen, Yi Zhang, Milica Hadzi-Tanovic, Grigore Rosu, Darko Marinov:
Techniques for Evolution-Aware Runtime Verification. ICST 2019: 300-311 - [c151]Xiaohong Chen, Grigore Rosu:
Matching μ-Logic. LICS 2019: 1-13 - [c150]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: 1133-1148 - [c149]Xiaohong Chen, Grigore Rosu:
$\mathbb {K}$ - A Semantic Framework for Programming Languages and Formal Analysis. SETSS 2019: 122-158 - [p2]Klaus Havelund, Giles Reger, Grigore Rosu:
Runtime Verification Past Experiences and Future Projections. Computing and Software Science 2019: 532-562 - [i6]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 abs/1907.05523 (2019) - 2018
- [j35]Grigore Rosu:
Finite-trace linear temporal logic: coinductive completeness. Formal Methods Syst. Des. 53(1): 138-163 (2018) - [c148]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: 204-217 - [c147]Brandon M. Moore, Lucas Peña, Grigore Rosu:
Program Verification by Coinduction. ESOP 2018: 589-618 - [c146]Xiaohong Chen, Grigore Rosu:
A Language-Independent Program Verification Framework. ISoLA (2) 2018: 92-102 - [c145]Xiaohong Chen, Daejun Park, Grigore Rosu:
A Language-Independent Approach to Smart Contract Verification. ISoLA (4) 2018: 405-413 - [c144]Grigore Rosu:
Formal Design, Implementation and Verification of Blockchain Languages (Invited Talk). FSCD 2018: 2:1-2:6 - [c143]Klaus Havelund, Grigore Rosu:
Runtime Verification - 17 Years Later. RV 2018: 3-17 - [c142]Daejun Park, Yi Zhang, Manasvi Saxena, Philip Daian, Grigore Rosu:
A formal verification tool for Ethereum VM bytecode. ESEC/SIGSOFT FSE 2018: 912-915 - [i5]Ali Kheradmand, Grigore Rosu:
P4K: A Formal Semantics of P4 and Applications. CoRR abs/1804.01468 (2018) - [i4]Andrei Stefanescu, Stefan Ciobaca, Radu Mereuta, Brandon M. Moore, Traian-Florin Serbanuta, Grigore Rosu:
All-Path Reachability Logic. CoRR abs/1810.10826 (2018) - 2017
- [j34]Grigore Rosu:
Matching Logic. Log. Methods Comput. Sci. 13(4) (2017) - [p1]Grigore Rosu:
𝕂: A Semantic Framework for Programming Languages and Formal Analysis Tools. Dependable Software Systems Engineering 2017: 186-206 - [e10]Grigore Rosu, Massimiliano Di Penta, Tien N. Nguyen:
Proceedings of the 32nd IEEE/ACM International Conference on Automated Software Engineering, ASE 2017, Urbana, IL, USA, October 30 - November 03, 2017. IEEE Computer Society 2017, ISBN 978-1-5386-2684-9 [contents] - [i3]Grigore Rosu:
Matching Logic. CoRR abs/1705.06312 (2017) - 2016
- [j33]Stefan Ciobaca, Dorel Lucanu, Vlad Rusu, Grigore Rosu:
A language-independent proof system for full program equivalence. Formal Aspects Comput. 28(3): 469-497 (2016) - [j32]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): 98-120 (2016) - [c141]Dorel Lucanu, Traian-Florin Serbanuta, Grigore Rosu:
Towards a \mathbb K K ool Future. Theory and Practice of Formal Methods 2016: 325-343 - [c140]Dwight Guth, Chris Hathhorn, Manasvi Saxena, Grigore Rosu:
RV-Match: Practical Semantics-Based Program Analysis. CAV (1) 2016: 447-453 - [c139]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: 602-613 - [c138]Andrei Stefanescu, Daejun Park, Shijiao Yuwen, Yilong Li, Grigore Rosu:
Semantics-based program verifiers for all languages. OOPSLA 2016: 74-91 - [c137]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: 46-67 - [c136]Grigore Rosu:
Finite-Trace Linear Temporal Logic: Coinductive Completeness. RV 2016: 333-350 - 2015
- [j31]Andrei Popescu, Grigore Rosu:
Term-generic logic. Theor. Comput. Sci. 577: 1-24 (2015) - [c135]Grigore Rosu:
From Rewriting Logic, to Programming Language Semantics, to Program Verification. Logic, Rewriting, and Concurrency 2015: 598-616 - [c134]Owolabi Legunsen, Darko Marinov, Grigore Rosu:
Evolution-Aware Monitoring-Oriented Programming. ICSE (2) 2015: 615-618 - [c133]Jeff Huang, Qingzhou Luo, Grigore Rosu:
GPredict: Generic Predictive Concurrency Analysis. ICSE (1) 2015: 847-857 - [c132]Chris Hathhorn, Chucky Ellison, Grigore Rosu:
Defining the undefinedness of C. PLDI 2015: 336-345 - [c131]Daejun Park, Andrei Stefanescu, Grigore Rosu:
KJS: a complete formal semantics of JavaScript. PLDI 2015: 346-356 - [c130]Denis Bogdanas, Grigore Rosu:
K-Java: A Complete Semantics of Java. POPL 2015: 445-456 - [c129]Grigore Rosu:
Matching Logic - Extended Abstract (Invited Talk). RTA 2015: 5-21 - [c128]Philip Daian, Yliès Falcone, Patrick O'Neil Meredith, Traian-Florin Serbanuta, Shinichi Shiraishi, Akihito Iwai, Grigore Rosu:
RV-Android: Efficient Parametric Android Runtime Verification, a Brief Tutorial. RV 2015: 342-357 - 2014
- [j30]Jörg Endrullis, Dimitri Hendriks, Rena Bakhshi, Grigore Rosu:
On the complexity of stream equality. J. Funct. Program. 24(2-3): 166-217 (2014) - [c127]Grigore Rosu, Dorel Lucanu:
Behavioral Rewrite Systems and Behavioral Productivity. Specification, Algebra, and Software 2014: 296-314 - [c126]Stefan Ciobaca, Dorel Lucanu, Vlad Rusu, Grigore Rosu:
A Language-Independent Proof System for Mutual Program Equivalence. ICFEM 2014: 75-90 - [c125]Jeff Huang, Patrick O'Neil Meredith, Grigore Rosu:
Maximal sound predictive race detection with control flow abstraction. PLDI 2014: 337-348 - [c124]Andrei Stefanescu, Stefan Ciobaca, Radu Mereuta, Brandon M. Moore, Traian-Florin Serbanuta, Grigore Rosu:
All-Path Reachability Logic. RTA-TLCA 2014: 425-440 - [c123]Jeff Huang, Cansu Erdogan, Yi Zhang, Brandon M. Moore, Qingzhou Luo, Aravind Sundaresan, Grigore Rosu:
ROSRV: Runtime Verification for Robots. RV 2014: 247-254 - [c122]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: 285-300 - [c121]Stefan Ciobaca, Dorel Lucanu, Vlad Rusu, Grigore Rosu:
A Theoretical Foundation for Programming Languages Aggregation. WADT 2014: 30-47 - [c120]Andrei Arusoaie, Dorel Lucanu, Vlad Rusu, Traian-Florin Serbanuta, Andrei Stefanescu, Grigore Rosu:
Language Definitions as Rewrite Theories. WRLA 2014: 97-112 - 2013
- [j29]José Meseguer, Grigore Rosu:
The rewriting logic semantics project: A progress report. Inf. Comput. 231: 38-69 (2013) - [c119]Qingzhou Luo, Grigore Rosu:
EnforceMOP: a runtime property enforcement system for multithreaded programs. ISSTA 2013: 156-166 - [c118]Patrick O'Neil Meredith, Grigore Rosu:
Efficient parametric runtime verification with deterministic string rewriting. ASE 2013: 70-80 - [c117]Grigore Rosu, Andrei Stefanescu, Stefan Ciobaca, Brandon M. Moore:
One-Path Reachability Logic. LICS 2013: 358-367 - [c116]Grigore Rosu:
Specifying Languages and Verifying Programs with K. SYNASC 2013: 28-31 - 2012
- [j28]Grigore Rosu, Feng Chen:
Semantics and Algorithms for Parametric Monitoring. Log. Methods Comput. Sci. 8(1) (2012) - [j27]Grigore Rosu:
On Safety Properties and Their Monitoring. Sci. Ann. Comput. Sci. 22(2): 327-365 (2012) - [j26]Oleg Sokolsky, Grigore Rosu:
Introduction to the special issue on runtime verification. Formal Methods Syst. Des. 41(3): 233-235 (2012) - [j25]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): 249-289 (2012) - [c115]David Lazar, Andrei Arusoaie, Traian-Florin Serbanuta, Chucky Ellison, Radu Mereuta, Dorel Lucanu, Grigore Rosu:
Executing Formal Semantics with the K Tool. FM 2012: 267-271 - [c114]Grigore Rosu, Andrei Stefanescu:
From Hoare Logic to Matching Logic Reachability. FM 2012: 387-402 - [c113]Traian-Florin Serbanuta, Grigore Rosu:
A Truly Concurrent Semantics for the K Framework Based on Graph Transformations. ICGT 2012: 294-310 - [c112]Grigore Rosu, Andrei Stefanescu:
Towards a Unified Theory of Operational and Axiomatic Semantics. ICALP (2) 2012: 351-363 - [c111]Dongyun Jin, Patrick O'Neil Meredith, Choonghwan Lee, Grigore Rosu:
JavaMOP: Efficient parametric runtime monitoring framework. ICSE 2012: 1427-1430 - [c110]Grigore Rosu, Andrei Stefanescu:
Checking reachability using matching logic. OOPSLA 2012: 555-574 - [c109]Soha Hussein, Patrick O'Neil Meredith, Grigore Rosu:
Security-policy monitoring and enforcement with JavaMOP. PLAS 2012: 3 - [c108]Chucky Ellison, Grigore Rosu:
An executable formal semantics of C with applications. POPL 2012: 533-544 - [c107]Traian-Florin Serbanuta, Feng Chen, Grigore Rosu:
Maximal Causal Models for Sequentially Consistent Systems. RV 2012: 136-150 - [c106]Dorel Lucanu, Traian-Florin Serbanuta, Grigore Rosu:
K Framework Distilled. WRLA 2012: 31-53 - [c105]Andrei Arusoaie, Traian-Florin Serbanuta, Chucky Ellison, Grigore Rosu:
Making Maude Definitions More Interactive. WRLA 2012: 83-98 - [e9]Holger Giese, Grigore Rosu:
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. Lecture Notes in Computer Science 7273, Springer 2012, ISBN 978-3-642-30792-8 [contents] - 2011
- [c104]José Meseguer, Grigore Rosu:
The Rewriting Logic Semantics Project: A Progress Report. FCT 2011: 1-37 - [c103]Choonghwan Lee, Feng Chen, Grigore Rosu:
Mining parametric specifications. ICSE 2011: 591-600 - [c102]Grigore Rosu, Andrei Stefanescu:
Matching logic: a new program verification approach. ICSE 2011: 868-871 - [c101]Dongyun Jin, Patrick O'Neil Meredith, Dennis Griffith, Grigore Rosu:
Garbage collection for monitoring parametric properties. PLDI 2011: 415-424 - [c100]Vilas Jagannath, Milos Gligoric, Dongyun Jin, Qingzhou Luo, Grigore Rosu, Darko Marinov:
Improved multithreaded unit testing. SIGSOFT FSE 2011: 223-233 - [c99]Grigore Rosu, Traian-Florin Serbanuta:
K Overview and SIMPLE Case Study. K 2011: 3-56 - [c98]Traian-Florin Serbanuta, Andrei Arusoaie, David Lazar, Chucky Ellison, Dorel Lucanu, Grigore Rosu:
The K Primer (version 3.3). K 2011: 57-80 - [c97]Codruta Gîrlea, Grigore Rosu:
Abstract Semantics for K Module Composition. K 2011: 127-149 - 2010
- [j24]Patrick O'Neil Meredith, Dongyun Jin, Feng Chen, Grigore Rosu:
Efficient monitoring of parametric context-free patterns. Autom. Softw. Eng. 17(2): 149-180 (2010) - [j23]Grigore Rosu, Traian-Florin Serbanuta:
An overview of the K semantic framework. J. Log. Algebraic Methods Program. 79(6): 397-434 (2010) - [c96]Grigore Rosu, Chucky Ellison, Wolfram Schulte:
Matching Logic: An Alternative to Hoare/Floyd Logic. AMAST 2010: 142-162 - [c95]Eugen-Ioan Goriac, Dorel Lucanu, Grigore Rosu:
Automating Coinduction with Case Analysis. ICFEM 2010: 220-236 - [c94]Vilas Jagannath, Milos Gligoric, Dongyun Jin, Grigore Rosu, Darko Marinov:
IMUnit: improved multithreaded unit testing. IWMSE@ICSE 2010: 48-49 - [c93]Patrick O'Neil Meredith, Michael Katelman, José Meseguer, Grigore Rosu:
A formal executable semantics of Verilog. MEMOCODE 2010: 179-188 - [c92]Mark Hills, Grigore Rosu:
A Rewriting Logic Semantics Approach to Modular Program Analysis. RTA 2010: 151-160 - [c91]Patrick O'Neil Meredith, Grigore Rosu:
Runtime Verification with the RV System. RV 2010: 136-152 - [c90]Traian-Florin Serbanuta, Grigore Rosu:
K-Maude: A Rewriting Based Tool for Semantics of Programming Languages. WRLA 2010: 104-122 - [e8]Howard Barringer, Yliès Falcone, Bernd Finkbeiner, Klaus Havelund, Insup Lee, Gordon J. Pace, Grigore Rosu, Oleg Sokolsky, Nikolai Tillmann:
Runtime Verification - First International Conference, RV 2010, St. Julians, Malta, November 1-4, 2010. Proceedings. Lecture Notes in Computer Science 6418, Springer 2010, ISBN 978-3-642-16611-2 [contents]
2000 – 2009
- 2009
- [j22]Traian-Florin Serbanuta, Grigore Rosu, José Meseguer:
A rewriting logic approach to operational semantics. Inf. Comput. 207(2): 305-340 (2009) - [j21]Andrei Popescu, Traian-Florin Serbanuta, Grigore Rosu:
A semantic approach to interpolation. Theor. Comput. Sci. 410(12-13): 1109-1128 (2009) - [c89]Eric Bodden, Feng Chen, Grigore Rosu:
Dependent advice: a general approach to optimizing history-based aspects. AOSD 2009: 3-14 - [c88]Grigore Rosu, Dorel Lucanu:
Circular Coinduction: A Proof Theoretical Foundation. CALCO 2009: 127-144 - [c87]Dorel Lucanu, Eugen-Ioan Goriac, Georgiana Caltais, Grigore Rosu:
CIRC: A Behavioral Verification Tool Based on Circular Coinduction. CALCO 2009: 433-442 - [c86]Dorel Lucanu, Grigore Rosu:
Circular Coinduction with Special Contexts. ICFEM 2009: 639-659 - [c85]Feng Chen, Patrick O'Neil Meredith, Dongyun Jin, Grigore Rosu:
Efficient Formalism-Independent Monitoring of Parametric Properties. ASE 2009: 383-394 - [c84]Grigore Rosu, Wolfram Schulte, Traian-Florin Serbanuta:
Runtime Verification of C Memory Safety. RV 2009: 132-151 - [c83]Feng Chen, Grigore Rosu:
Parametric Trace Slicing and Monitoring. TACAS 2009: 246-261 - [e7]Grigore Rosu:
Proceedings of the Seventh International Workshop on Rewriting Logic and its Applications, WRLA 2008, Budapest, Hungary, March 29-30, 2008. Electronic Notes in Theoretical Computer Science 238(3), Elsevier 2009 [contents] - 2008
- [c82]Feng Chen, Traian-Florin Serbanuta, Grigore Rosu:
jPredictor: a predictive runtime analysis tool for java. ICSE 2008: 221-230 - [c81]Patrick O'Neil Meredith, Dongyun Jin, Feng Chen, Grigore Rosu:
Efficient Monitoring of Parametric Context-Free Patterns. ASE 2008: 148-157 - [c80]Traian Serbanuta, Gheorghe Stefanescu, Grigore Rosu:
Defining and Executing P Systems with Structured Data in K. Workshop on Membrane Computing 2008: 374-393 - [c79]Rodolfo Pellizzoni, Patrick O'Neil Meredith, Marco Caccamo, Grigore Rosu:
Hardware Runtime Monitoring for Dependable COTS-Based Real-Time Embedded Systems. RTSS 2008: 481-491 - [c78]Grigore Rosu, Feng Chen, Thomas Ball:
Synthesizing Monitors for Safety Properties: This Time with Calls and Returns. RV 2008: 51-68 - [c77]Chucky Ellison, Traian-Florin Serbanuta, Grigore Rosu:
A Rewriting Logic Approach to Type Inference. WADT 2008: 135-151 - [c76]Mark Hills, Grigore Rosu:
Towards a Module System for K. WADT 2008: 187-205 - [c75]Andrei Popescu, Grigore Rosu:
Term-Generic Logic. WADT 2008: 290-307 - [c74]Grigore Rosu:
Preface. WRLA 2008: 1-3 - [c73]Mark Hills, Feng Chen, Grigore Rosu:
A Rewriting Logic Approach to Static Checking of Units of Measurement in C. RULE 2008: 51-67 - [e6]José Meseguer, Grigore Rosu:
Algebraic Methodology and Software Technology, 12th International Conference, AMAST 2008, Urbana, IL, USA, July 28-31, 2008, Proceedings. Lecture Notes in Computer Science 5140, Springer 2008, ISBN 978-3-540-79979-5 [contents] - [e5]Bernd Finkbeiner, Klaus Havelund, Grigore Rosu, Oleg Sokolsky:
Runtime Verification, 02.01. - 06.01.2007. Dagstuhl Seminar Proceedings 07011, Internationales Begegnungs- und Forschungszentrum fuer Informatik (IBFI), Schloss Dagstuhl, Germany 2008 [contents] - 2007
- [j20]Grigore Rosu, Koushik Sen:
An instrumentation technique for online analysis of multithreaded programs. Concurr. Comput. Pract. Exp. 19(3): 311-325 (2007) - [j19]Narciso Martí-Oliet, Grigore Rosu, Carolyn L. Talcott:
Editorial. High. Order Symb. Comput. 20(1-2): 1-2 (2007) - [j18]José Meseguer, Grigore Rosu:
The rewriting logic semantics project. Theor. Comput. Sci. 373(3): 213-237 (2007) - [c72]Dorel Lucanu, Grigore Rosu:
CIRC : A Circular Coinductive Prover. CALCO 2007: 372-378 - [c71]Feng Chen, Grigore Rosu:
Parametric and Sliced Causality. CAV 2007: 240-253 - [c70]Mark Hills, Grigore Rosu:
On Formal Analysis of OO Languages Using Rewriting Logic: Designing for Performance. FMOODS 2007: 107-121 - [c69]Grigore Rosu:
An Effective Algorithm for the Membership Problem for Extended Regular Expressions. FoSSaCS 2007: 332-345 - [c68]Feng Chen, Grigore Rosu:
Mop: an efficient and generic runtime verification framework. OOPSLA 2007: 569-588 - [c67]Mark Hills, Grigore Rosu:
A rewriting approach to the design and evolution of object-oriented languages. OOPSLA Companion 2007: 827-828 - [c66]Mark Hills, Grigore Rosu:
KOOL: An Application of Rewriting Logic to Language Prototyping and Analysis. RTA 2007: 246-256 - [c65]Dorel Lucanu, Grigore Rosu, Gheorghe Grigoras:
Regular Strategies as Proof Tactics for CIRC. WRS@RDP 2007: 83-98 - [c64]Traian-Florin Serbanuta, Grigore Rosu, José Meseguer:
A Rewriting Logic Approach to Operational Semantics (Extended Abstract). SOS@LICS/ICALP 2007: 125-141 - [i2]Bernd Finkbeiner, Klaus Havelund, Grigore Rosu, Oleg Sokolsky:
07011 Executive Summary -- Runtime Verification. Runtime Verification 2007 - [i1]Bernd Finkbeiner, Klaus Havelund, Grigore Rosu, Oleg Sokolsky:
07011 Abstracts Collection -- Runtime Verification. Runtime Verification 2007 - 2006
- [j17]Koushik Sen, Grigore Rosu, Gul Agha:
Online efficient predictive safety analysis of multithreaded programs. Int. J. Softw. Tools Technol. Transf. 8(3): 248-260 (2006) - [c63]Grigore Rosu:
Complete Categorical Deduction for Satisfaction as Injectivity. Essays Dedicated to Joseph A. Goguen 2006: 157-172 - [c62]Grigore Rosu, Saddek Bensalem:
Allen Linear (Interval) Temporal Logic - Translation to LTL and Monitor Synthesis. CAV 2006: 263-277 - [c61]Sumant Kowshik, Grigore Rosu, Lui Sha:
Static Analysis to Enforce Safe Value Flow in Embedded Control Systems. DSN 2006: 23-34 - [c60]Andrei Popescu, Traian Serbanuta, Grigore Rosu:
A Semantic Approach to Interpolation. FoSSaCS 2006: 307-321 - [c59]Grigore Rosu:
Equality of streams is a Pi0 over 2-complete problem. ICFP 2006: 184-191 - [c58]Koushik Sen, Abhay Vardhan, Gul Agha, Grigore Rosu:
Decentralized runtime analysis of multithreaded applications. IPDPS 2006 - [c57]Traian-Florin Serbanuta, Grigore Rosu:
Computationally Equivalent Elimination of Conditions. RTA 2006: 19-34 - [c56]Feng Chen, Grigore Rosu:
Parametric and Termination-Sensitive Control Dependence. SAS 2006: 387-404 - [c55]Mark Hills, Traian Serbanuta, Grigore Rosu:
A Rewrite Framework for Language Definitions and for Generation of Efficient Interpreters. WRLA 2006: 215-231 - [c54]Grit Denker, Carolyn L. Talcott, Grigore Rosu, Mark van den Brand, Steven Eker, Traian-Florin Serbanuta:
Rewriting Logic Systems. WRLA 2006: 233-247 - [e4]Klaus Havelund, Manuel Núñez, Grigore Rosu, Burkhart Wolff:
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. Lecture Notes in Computer Science 4262, Springer 2006, ISBN 3-540-49699-8 [contents] - 2005
- [j16]Grigore Rosu, Klaus Havelund:
Rewriting-Based Techniques for Runtime Verification. Autom. Softw. Eng. 12(2): 151-197 (2005) - [j15]Klaus Havelund, Grigore Rosu:
Foreword. Formal Methods Syst. Des. 27(3): 211-212 (2005) - [j14]Marcelo d'Amorim, Grigore Rosu:
An Equational Specification for the Scheme Language. J. Univers. Comput. Sci. 11(7): 1327-1348 (2005) - [j13]Cyrille Artho, Howard Barringer, Allen Goldberg, Klaus Havelund, Sarfraz Khurshid, Michael R. Lowry, Corina S. Pasareanu, Grigore Rosu, Koushik Sen, Willem Visser, Richard Washington:
Combining test case generation and runtime verification. Theor. Comput. Sci. 336(2-3): 209-234 (2005) - [c53]Andrei Popescu, Grigore Rosu:
Behavioral Extensions of Institutions. CALCO 2005: 331-347 - [c52]Marcelo d'Amorim, Grigore Rosu:
Efficient Monitoring of omega-Languages. CAV 2005: 364-378 - [c51]Pierre Salverda, Grigore Rosu, Craig B. Zilles:
Formally Defining and Verifying Master/Slave Speculative Parallelization. FM 2005: 123-138 - [c50]Koushik Sen, Grigore Rosu, Gul Agha:
Detecting Errors in Multithreaded Programs by Generalized Predictive Analysis of Executions. FMOODS 2005: 211-226 - [c49]Florin Baboescu, Dean M. Tullsen, Grigore Rosu, Sumeet Singh:
A Tree Based Router Search Engine Architecture with Single Port Memories. ISCA 2005: 123-133 - [c48]Feng Chen, Grigore Rosu:
Java-MOP: A Monitoring Oriented Programming Environment for Java. TACAS 2005: 546-550 - [c47]José Meseguer, Grigore Rosu:
Computational Logical Frameworks and Generic Program Analysis Technologies. VSTTE 2005: 256-267 - [c46]Feng Chen, Marcelo d'Amorim, Grigore Rosu:
Checking and Correcting Behaviors of Java Programs at Runtime with Java-MOP. RV@CAV 2005: 3-20 - [c45]José Meseguer, Grigore Rosu:
The Rewriting Logic Semantics Project. SOS@ICALP 2005: 27-56 - [e3]Klaus Havelund, Grigore Rosu:
Proceedings of the Fourth Workshop on Runtime Verification, RV@ETAPS 2004, Barcelona, Spain, April 3, 2004. Electronic Notes in Theoretical Computer Science 113, Elsevier 2005 [contents] - 2004
- [j12]Klaus Havelund, Grigore Rosu:
Foreword - Selected Papers from the First International Workshop on Runtime Verification held in Paris, July 2001 (RV'01). Formal Methods Syst. Des. 24(2): 99-100 (2004) - [j11]Klaus Havelund, Grigore Rosu:
An Overview of the Runtime Verification Tool Java PathExplorer. Formal Methods Syst. Des. 24(2): 189-215 (2004) - [j10]Klaus Havelund, Grigore Rosu:
Efficient monitoring of safety properties. Int. J. Softw. Tools Technol. Transf. 6(2): 158-173 (2004) - [j9]Grigore Rosu:
Behavioral abstraction is hiding information. Theor. Comput. Sci. 327(1-2): 197-221 (2004) - [c44]Azadeh Farzan, José Meseguer, Grigore Rosu:
Formal JVM Code Analysis in JavaFAN. AMAST 2004: 132-147 - [c43]Joseph A. Goguen, Grigore Rosu:
Composing Hidden Information Modules over Inclusive Institutions. Essays in Memory of Ole-Johan Dahl 2004: 96-123 - [c42]José Meseguer, Grigore Rosu:
Rewriting Logic Semantics: From Language Specifications to Formal Analysis Tools. IJCAR 2004: 1-44 - [c41]Azadeh Farzan, Feng Chen, José Meseguer, Grigore Rosu:
Formal Analysis of Java Programs in JavaFAN. CAV 2004: 501-505 - [c40]Grigore Rosu:
Extensional Theories and Rewriting. ICALP 2004: 1066-1079 - [c39]Feng Chen, Marcelo d'Amorim, Grigore Rosu:
A Formal Monitoring-Based Framework for Software Development and Analysis. ICFEM 2004: 357-372 - [c38]Koushik Sen, Abhay Vardhan, Gul Agha, Grigore Rosu:
Efficient Decentralized Monitoring of Safety in Distributed Systems. ICSE 2004: 418-427 - [c37]Grigore Rosu, Koushik Sen:
An Instrumentation Technique for Online Analysis of Multithreaded Programs. IPDPS 2004 - [c36]Koushik Sen, Grigore Rosu, Gul Agha:
Online Efficient Predictive Safety Analysis of Multithreaded Programs. TACAS 2004: 123-138 - [c35]Grigore Rosu:
From Conditional to Unconditional Rewriting. WADT 2004: 218-233 - [c34]Klaus Havelund, Grigore Rosu:
Preface. RV@ETAPS 2004: 1-2 - [c33]Prasanna Thati, Grigore Rosu:
Monitoring Algorithms for Metric Temporal Logic Specifications. RV@ETAPS 2004: 145-162 - 2003
- [c32]Koushik Sen, Grigore Rosu, Gul Agha:
Generating Optimal Linear Temporal Logic Monitors by Coinduction. ASIAN 2003: 260-275 - [c31]Cyrille Artho, Doron Drusinsky, Allen Goldberg, Klaus Havelund, Michael R. Lowry, Corina S. Pasareanu, Grigore Rosu, Willem Visser:
Experiments with Test Case Generation and Runtime Analysis. Abstract State Machines 2003: 87-107 - [c30]Grigore Rosu, Ram Prasad Venkatesan, Jon Whittle, Laurentiu Leustean:
Certifying Optimality of State Estimation Programs. CAV 2003: 301-314 - [c29]Grigore Rosu, Steven Eker, Patrick Lincoln, José Meseguer:
Certifying and Synthesizing Membership Equational Proofs. FME 2003: 359-380 - [c28]Grigore Rosu, Feng Chen:
Certifying Measurement Unit Safety Polic. ASE 2003: 304-309 - [c27]Feng Chen, Grigore Rosu, Ram Prasad Venkatesan:
Rule-Based Analysis of Dimensional Safety. RTA 2003: 197-207 - [c26]Grigore Rosu, Mahesh Viswanathan:
Testing Extended Regular Language Membership Incrementally by Rewriting. RTA 2003: 499-514 - [c25]Koushik Sen, Grigore Rosu, Gul Agha:
Runtime safety analysis of multithreaded programs. ESEC / SIGSOFT FSE 2003: 337-346 - [c24]Feng Chen, Grigore Rosu:
Towards Monitoring-Oriented Programming: A Paradigm Combining Specification and Implementation. RV@CAV 2003: 108-127 - [c23]Koushik Sen, Grigore Rosu:
Generating Optimal Monitors for Extended Regular Expressions. RV@CAV 2003: 226-245 - [c22]Grigore Rosu:
Inductive Behavioral Proofs by Unhiding. CMCS 2003: 285-302 - 2002
- [j8]Joseph A. Goguen, Grigore Rosu:
Institution Morphisms. Formal Aspects Comput. 13(3-5): 274-307 (2002) - [j7]Grigore Rosu:
Axiomatizability in Inclusive Equational Logics. Math. Struct. Comput. Sci. 12(5): 541-563 (2002) - [c21]José Meseguer, Grigore Rosu:
A Total Approach to Partial Algebraic Specification. ICALP 2002: 572-584 - [c20]Grigore Rosu, Jon Whittle:
Towards Certifying Domain-Specific Properties of Synthesized Code. ASE 2002: 289-294 - [c19]Grigore Rosu:
On implementing behavioral rewriting. ACM SIGPLAN Workshop on Rule-Based Programming 2002: 43-52 - [c18]Klaus Havelund, Grigore Rosu:
Synthesizing Monitors for Safety Properties. TACAS 2002: 342-356 - [c17]Joseph A. Goguen, Kai Lin, Grigore Rosu:
Conditional Circular Coinductive Rewriting with Case Analysis. WADT 2002: 216-232 - [c16]José Meseguer, Grigore Rosu:
Towards Behavioral Maude: Behavioral Membership Equational Logic. CMCS 2002: 197-253 - [c15]Klaus Havelund, Grigore Rosu:
Preface. RV@FLoC 2002: 201-202 - [e2]Klaus Havelund, Grigore Rosu:
Runtime Verification 2002, RV 2002, FLoC Satellite Event, Copenhagen, Denmark, July 26, 2002. Electronic Notes in Theoretical Computer Science 70(4), Elsevier 2002 [contents] - 2001
- [j6]Grigore Rosu:
Equational axiomatizability for coalgebra. Theor. Comput. Sci. 260(1-2): 229-247 (2001) - [c14]Grigore Rosu:
Complete Categorical Equational Deduction. CSL 2001: 528-538 - [c13]Michael R. Lowry, Thomas Pressburger, Grigore Rosu:
Certifying Domain-Specific Policies. ASE 2001: 81-90 - [c12]Klaus Havelund, Grigore Rosu:
Monitoring Programs Using Rewriting. ASE 2001: 135-143 - [c11]Klaus Havelund, Grigore Rosu:
Monitoring Java Programs with Java PathExplorer. RV@CAV 2001: 200-217 - [c10]Klaus Havelund, Grigore Rosu:
Preface. RV@CAV 2001: 287-288 - [c9]Bernd Fischer, Grigore Rosu:
Interpreting Abstract Interpretations in Membership Equational Logic. RULE@PLI 2001: 271-285 - [e1]Klaus Havelund, Grigore Rosu:
Workshop on Runtime Verification, RV 2001, in connection with CAV 2001, Paris, France, July 23, 2001. Electronic Notes in Theoretical Computer Science 55(2), Elsevier 2001 [contents] - 2000
- [j5]Virgil Emil Cazanescu, Grigore Rosu:
Weak Inclusion Systems: Part Two. J. Univers. Comput. Sci. 6(1): 5-21 (2000) - [j4]Grigore Rosu, Joseph A. Goguen:
On Equational Craig Interpolation. J. Univers. Comput. Sci. 6(1): 194-200 (2000) - [c8]Joseph A. Goguen, Kai Lin, Grigore Rosu:
Circular Coinductive Rewriting. ASE 2000: 123-132 - [c7]Joseph A. Goguen, Kai Lin, Grigore Rosu:
Behavioral and Coinductive Rewriting. WRLA 2000: 2-23 - [c6]Samuel R. Buss, Grigore Rosu:
Incompleteness of Behavioral Logics. CMCS 2000: 61-79
1990 – 1999
- 1999
- [j3]Grigore Rosu:
Kan Extensions of Institutions. J. Univers. Comput. Sci. 5(8): 482-493 (1999) - [c5]Joseph A. Goguen, Grigore Rosu:
Hiding More of Hidden Algebra. World Congress on Formal Methods 1999: 1704-1719 - [c4]Joseph A. Goguen, Grigore Rosu:
A protocol for distributed cooperative work. WDS@FCT 1999: 3 - 1998
- [c3]Grigore Rosu, Joseph A. Goguen:
Hidden Congruent Deduction. FTP (LNCS Selection) 1998: 251-266 - [c2]Grigore Rosu:
A Birkhoff-like Axiomatizability Result for Hidden Algebra and Coalgebra. CMCS 1998: 176-193 - 1997
- [j2]Virgil Emil Cazanescu, Grigore Rosu:
Weak Inclusion Systems. Math. Struct. Comput. Sci. 7(2): 195-206 (1997) - [c1]Joseph A. Goguen, Kai Lin, Akira Mori, Grigore Rosu, Akiyoshi Sato:
Distributed Cooperative Formal Methods Tools. ASE 1997: 55-62 - 1994
- [j1]Grigore Rosu:
The Institution of Order-Sorted Equational Logic. Bull. EATCS 53: 250-255 (1994)
Coauthor Index
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
Unpaywalled article links
Add open access links from 
to the list of external document links (if available).
Privacy notice: By enabling the option above, your browser will contact the API of unpaywall.org to load hyperlinks to open access articles. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Unpaywall privacy policy.
Archived links via Wayback Machine
For web page which are no longer available, try to retrieve content from the 
of the Internet Archive (if available).
Privacy notice: By enabling the option above, your browser will contact the API of archive.org to check for archived content of web pages that are no longer available. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Internet Archive privacy policy.
Reference lists
Add a list of references from 
, 
, and 
to record detail pages.
load references from crossref.org and opencitations.net
Privacy notice: By enabling the option above, your browser will contact the APIs of crossref.org, opencitations.net, and semanticscholar.org to load article reference information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Crossref privacy policy and the OpenCitations privacy policy, as well as the AI2 Privacy Policy covering Semantic Scholar.
Citation data
Add a list of citing articles from and to record detail pages.
load citations from opencitations.net
Privacy notice: By enabling the option above, your browser will contact the API of opencitations.net and semanticscholar.org to load citation information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the OpenCitations privacy policy as well as the AI2 Privacy Policy covering Semantic Scholar.
OpenAlex data
Load additional information about publications from 
.
Privacy notice: By enabling the option above, your browser will contact the API of openalex.org to load additional information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the information given by OpenAlex.
last updated on 2024-10-31 21:08 CET by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by:
