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. Version 0.2. Zenodo, 2022 [all versions]
- [d6]Zhengyao Lin, Xiaohong Chen, Minh-Thai Trinh, John Wang, Grigore Rosu:
Generating Proof Certificates for a Language-Agnostic Deductive Program Verifier. Version 0.3. Zenodo, 2022 [all versions] - [d5]Zhengyao Lin, Xiaohong Chen, Minh-Thai Trinh, John Wang, Grigore Rosu:
Generating Proof Certificates for a Language-Agnostic Deductive Program Verifier. Version 0.4. Zenodo, 2022 [all versions] - [d4]Zhengyao Lin, Xiaohong Chen, Minh-Thai Trinh, John Wang, Grigore Rosu:
Generating Proof Certificates for a Language-Agnostic Deductive Program Verifier. Version 0.5. Zenodo, 2022 [all versions] - 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. Version 0.0.1. Zenodo, 2021 [all versions] - [d2]Xiaohong Chen, Zhengyao Lin, Minh-Thai Trinh, Grigore Rosu:
Towards a Trustworthy Semantics-Based Language Framework via Proof Generation. Version 0.0.1. Zenodo, 2021 [all versions] - [d1]Xiaohong Chen, Zhengyao Lin, Minh-Thai Trinh, Grigore Rosu:
Towards a Trustworthy Semantics-Based Language Framework via Proof Generation. Version 0.0.3. Zenodo, 2021 [all versions] - [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]