Stop the war!Остановите войну!
for scientists:
Google
Google Scholar
Semantic Scholar
IA Scholar
CiteSeerX
ORCIDGrigore Rosu
Person information
- affiliation: University of Illinois, USA
Refine list
refinements active!
zoomed in on ?? of ?? records
view refined list in
export refined list as
showing all ?? records
2020 – today
- 2022
[e10]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]- [e9]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] - [e8]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] - 2021
- [j59]Xiaohong Chen, Dorel Lucanu, Grigore Rosu:
Matching logic explained. J. Log. Algebraic Methods Program. 120: 100638 (2021) - [c147]Theodoros Kasampalis, Daejun Park, Zhengyao Lin, Vikram S. Adve, Grigore Rosu:
Language-parametric compiler validation with application to LLVM. ASPLOS 2021: 1004-1019 - [c146]Xiaohong Chen, Grigore Rosu:
The K Vision for the Future of Programming Language Design and Analysis. Formal Methods in Outer Space 2021: 3-9 - [c145]Xiaohong Chen, Zhengyao Lin, Minh-Thai Trinh, Grigore Rosu:
Towards a Trustworthy Semantics-Based Language Framework via Proof Generation. CAV (2) 2021: 477-499 - [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
- [j58]Xiaohong Chen, Grigore Rosu:
A general approach to define binders using matching logic. Proc. ACM Program. Lang. 4(ICFP): 88:1-88:32 (2020) - [j57]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) - [c144]Grigore Rosu:
Formal Design, Implementation and Verification of Blockchain Languages Using K (Invited Talk). FMBC@CAV 2020: 1:1-1:1 - [c143]Daejun Park, Yi Zhang, Grigore Rosu:
End-to-End Formal Verification of Ethereum 2.0 Deposit Smart Contract. CAV (1) 2020: 151-164 - [c142]Grigore Rosu, Xiaohong Chen:
Matching logic: the foundation of the K framework (invited talk). CPP 2020: 1 - [c141]Elaine Li, Traian Serbanuta, Denisa Diaconescu, Vlad Zamfir, Grigore Rosu:
Formalizing Correct-by-Construction Casper in Coq. IEEE ICBC 2020: 1-3 - [c140]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
- [j56]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) - [j55]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) - [j54]Chris Hathhorn, Grigore Rosu:
Dealing With C's Original Sin. IEEE Softw. 36(5): 24-28 (2019) - [j53]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) - [c139]Xiaohong Chen, Grigore Rosu:
Matching mu-Logic: Foundation of K Framework (Invited Paper). CALCO 2019: 1:1-1:4 - [c138]Musab A. Alturki, Grigore Rosu:
Statistical Model Checking of RANDAO's Resilience to Pre-computed Reveal Strategies. FM Workshops (1) 2019: 337-349 - [c137]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 - [c136]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 - [c135]Owolabi Legunsen, Yi Zhang, Milica Hadzi-Tanovic, Grigore Rosu, Darko Marinov:
Techniques for Evolution-Aware Runtime Verification. ICST 2019: 300-311 - [c134]Xiaohong Chen, Grigore Rosu:
Matching μ-Logic. LICS 2019: 1-13 - [c133]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 - [c132]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
- [j52]Grigore Rosu:
Finite-trace linear temporal logic: coinductive completeness. Formal Methods Syst. Des. 53(1): 138-163 (2018) - [c131]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 - [c130]Brandon M. Moore, Lucas Peña, Grigore Rosu:
Program Verification by Coinduction. ESOP 2018: 589-618 - [c129]Xiaohong Chen, Grigore Rosu:
A Language-Independent Program Verification Framework. ISoLA (2) 2018: 92-102 - [c128]Xiaohong Chen, Daejun Park, Grigore Rosu:
A Language-Independent Approach to Smart Contract Verification. ISoLA (4) 2018: 405-413 - [c127]Grigore Rosu:
Formal Design, Implementation and Verification of Blockchain Languages (Invited Talk). FSCD 2018: 2:1-2:6 - [c126]Klaus Havelund, Grigore Rosu:
Runtime Verification - 17 Years Later. RV 2018: 3-17 - [c125]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
- [j51]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 - [e7]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
- [j50]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) - [j49]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) - [c124]Dorel Lucanu, Traian-Florin Serbanuta, Grigore Rosu:
Towards a \mathbb K K ool Future. Theory and Practice of Formal Methods 2016: 325-343 - [c123]Dwight Guth, Chris Hathhorn, Manasvi Saxena, Grigore Rosu:
RV-Match: Practical Semantics-Based Program Analysis. CAV (1) 2016: 447-453 - [c122]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 - [c121]Andrei Stefanescu, Daejun Park, Shijiao Yuwen, Yilong Li, Grigore Rosu:
Semantics-based program verifiers for all languages. OOPSLA 2016: 74-91 - [c120]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 - [c119]Grigore Rosu:
Finite-Trace Linear Temporal Logic: Coinductive Completeness. RV 2016: 333-350 - 2015
- [j48]Andrei Popescu, Grigore Rosu:
Term-generic logic. Theor. Comput. Sci. 577: 1-24 (2015) - [c118]Grigore Rosu:
From Rewriting Logic, to Programming Language Semantics, to Program Verification. Logic, Rewriting, and Concurrency 2015: 598-616 - [c117]Owolabi Legunsen, Darko Marinov, Grigore Rosu:
Evolution-Aware Monitoring-Oriented Programming. ICSE (2) 2015: 615-618 - [c116]Jeff Huang, Qingzhou Luo, Grigore Rosu:
GPredict: Generic Predictive Concurrency Analysis. ICSE (1) 2015: 847-857 - [c115]Chris Hathhorn, Chucky Ellison, Grigore Rosu:
Defining the undefinedness of C. PLDI 2015: 336-345 - [c114]Daejun Park, Andrei Stefanescu, Grigore Rosu:
KJS: a complete formal semantics of JavaScript. PLDI 2015: 346-356 - [c113]Denis Bogdanas, Grigore Rosu:
K-Java: A Complete Semantics of Java. POPL 2015: 445-456 - [c112]Grigore Rosu:
Matching Logic - Extended Abstract (Invited Talk). RTA 2015: 5-21 - [c111]Philip Daian, Yliès Falcone, Patrick O'Neil Meredith, Traian-Florin Serbanuta, Shinichi Shiriashi, Akihito Iwai, Grigore Rosu:
RV-Android: Efficient Parametric Android Runtime Verification, a Brief Tutorial. RV 2015: 342-357 - 2014
- [j47]Grigore Rosu, Traian-Florin Serbanuta:
K Overview and SIMPLE Case Study. Electron. Notes Theor. Comput. Sci. 304: 3-56 (2014) - [j46]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: 57-80 (2014) - [j45]Codruta Gîrlea, Grigore Rosu:
Abstract Semantics for K Module Composition. Electron. Notes Theor. Comput. Sci. 304: 127-149 (2014) - [j44]Jörg Endrullis, Dimitri Hendriks, Rena Bakhshi, Grigore Rosu:
On the complexity of stream equality. J. Funct. Program. 24(2-3): 166-217 (2014) - [c110]Grigore Rosu, Dorel Lucanu:
Behavioral Rewrite Systems and Behavioral Productivity. Specification, Algebra, and Software 2014: 296-314 - [c109]Stefan Ciobaca, Dorel Lucanu, Vlad Rusu, Grigore Rosu:
A Language-Independent Proof System for Mutual Program Equivalence. ICFEM 2014: 75-90 - [c108]Jeff Huang, Patrick O'Neil Meredith, Grigore Rosu:
Maximal sound predictive race detection with control flow abstraction. PLDI 2014: 337-348 - [c107]Andrei Stefanescu, Stefan Ciobaca, Radu Mereuta, Brandon M. Moore, Traian-Florin Serbanuta, Grigore Rosu:
All-Path Reachability Logic. RTA-TLCA 2014: 425-440 - [c106]Jeff Huang, Cansu Erdogan, Yi Zhang, Brandon M. Moore, Qingzhou Luo, Aravind Sundaresan, Grigore Rosu:
ROSRV: Runtime Verification for Robots. RV 2014: 247-254 - [c105]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 - [c104]Stefan Ciobaca, Dorel Lucanu, Vlad Rusu, Grigore Rosu:
A Theoretical Foundation for Programming Languages Aggregation. WADT 2014: 30-47 - [c103]Andrei Arusoaie, Dorel Lucanu, Vlad Rusu, Traian-Florin Serbanuta, Andrei Stefanescu, Grigore Rosu:
Language Definitions as Rewrite Theories. WRLA 2014: 97-112 - 2013
- [j43]José Meseguer, Grigore Rosu:
The rewriting logic semantics project: A progress report. Inf. Comput. 231: 38-69 (2013) - [c102]Qingzhou Luo, Grigore Rosu:
EnforceMOP: a runtime property enforcement system for multithreaded programs. ISSTA 2013: 156-166 - [c101]Patrick O'Neil Meredith, Grigore Rosu:
Efficient parametric runtime verification with deterministic string rewriting. ASE 2013: 70-80 - [c100]Grigore Rosu, Andrei Stefanescu, Stefan Ciobaca, Brandon M. Moore:
One-Path Reachability Logic. LICS 2013: 358-367 - [c99]Grigore Rosu:
Specifying Languages and Verifying Programs with K. SYNASC 2013: 28-31 - 2012
- [j42]Grigore Rosu, Feng Chen:
Semantics and Algorithms for Parametric Monitoring. Log. Methods Comput. Sci. 8(1) (2012) - [j41]Grigore Rosu:
On Safety Properties and Their Monitoring. Sci. Ann. Comput. Sci. 22(2): 327-365 (2012) - [j40]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: 51-67 (2012) - [j39]Oleg Sokolsky, Grigore Rosu:
Introduction to the special issue on runtime verification. Formal Methods Syst. Des. 41(3): 233-235 (2012) - [j38]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) - [c98]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 - [c97]Grigore Rosu, Andrei Stefanescu:
From Hoare Logic to Matching Logic Reachability. FM 2012: 387-402 - [c96]Traian-Florin Serbanuta, Grigore Rosu:
A Truly Concurrent Semantics for the K Framework Based on Graph Transformations. ICGT 2012: 294-310 - [c95]Grigore Rosu, Andrei Stefanescu:
Towards a Unified Theory of Operational and Axiomatic Semantics. ICALP (2) 2012: 351-363 - [c94]Dongyun Jin, Patrick O'Neil Meredith, Choonghwan Lee, Grigore Rosu:
JavaMOP: Efficient parametric runtime monitoring framework. ICSE 2012: 1427-1430 - [c93]Grigore Rosu, Andrei Stefanescu:
Checking reachability using matching logic. OOPSLA 2012: 555-574 - [c92]Soha Hussein, Patrick O'Neil Meredith, Grigore Rosu:
Security-policy monitoring and enforcement with JavaMOP. PLAS 2012: 3 - [c91]Chucky Ellison, Grigore Rosu:
An executable formal semantics of C with applications. POPL 2012: 533-544 - [c90]Traian-Florin Serbanuta, Feng Chen, Grigore Rosu:
Maximal Causal Models for Sequentially Consistent Systems. RV 2012: 136-150 - [c89]Dorel Lucanu, Traian-Florin Serbanuta, Grigore Rosu:
K Framework Distilled. WRLA 2012: 31-53 - [c88]Andrei Arusoaie, Traian-Florin Serbanuta, Chucky Ellison, Grigore Rosu:
Making Maude Definitions More Interactive. WRLA 2012: 83-98 - [e6]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
- [c87]José Meseguer, Grigore Rosu:
The Rewriting Logic Semantics Project: A Progress Report. FCT 2011: 1-37 - [c86]Choonghwan Lee, Feng Chen, Grigore Rosu:
Mining parametric specifications. ICSE 2011: 591-600 - [c85]Grigore Rosu, Andrei Stefanescu:
Matching logic: a new program verification approach. ICSE 2011: 868-871 - [c84]Dongyun Jin, Patrick O'Neil Meredith, Dennis Griffith, Grigore Rosu:
Garbage collection for monitoring parametric properties. PLDI 2011: 415-424 - [c83]Vilas Jagannath, Milos Gligoric, Dongyun Jin, Qingzhou Luo, Grigore Rosu, Darko Marinov:
Improved multithreaded unit testing. SIGSOFT FSE 2011: 223-233 - 2010
- [j37]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) - [j36]Grigore Rosu, Traian-Florin Serbanuta:
An overview of the K semantic framework. J. Log. Algebraic Methods Program. 79(6): 397-434 (2010) - [c82]Grigore Rosu, Chucky Ellison, Wolfram Schulte:
Matching Logic: An Alternative to Hoare/Floyd Logic. AMAST 2010: 142-162 - [c81]Eugen-Ioan Goriac, Dorel Lucanu, Grigore Rosu:
Automating Coinduction with Case Analysis. ICFEM 2010: 220-236 - [c80]Vilas Jagannath, Milos Gligoric, Dongyun Jin, Grigore Rosu, Darko Marinov:
IMUnit: improved multithreaded unit testing. IWMSE@ICSE 2010: 48-49 - [c79]Patrick O'Neil Meredith, Michael Katelman, José Meseguer, Grigore Rosu:
A formal executable semantics of Verilog. MEMOCODE 2010: 179-188 - [c78]Mark Hills, Grigore Rosu:
A Rewriting Logic Semantics Approach to Modular Program Analysis. RTA 2010: 151-160 - [c77]Patrick O'Neil Meredith, Grigore Rosu:
Runtime Verification with the RV System. RV 2010: 136-152 - [c76]Traian-Florin Serbanuta, Grigore Rosu:
K-Maude: A Rewriting Based Tool for Semantics of Programming Languages. WRLA 2010: 104-122 - [e5]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
- [j35]Traian-Florin Serbanuta, Grigore Rosu, José Meseguer:
A rewriting logic approach to operational semantics. Inf. Comput. 207(2): 305-340 (2009) - [j34]Andrei Popescu, Traian-Florin Serbanuta, Grigore Rosu:
A semantic approach to interpolation. Theor. Comput. Sci. 410(12-13): 1109-1128 (2009) - [c75]Eric Bodden, Feng Chen, Grigore Rosu:
Dependent advice: a general approach to optimizing history-based aspects. AOSD 2009: 3-14 - [c74]Grigore Rosu, Dorel Lucanu:
Circular Coinduction: A Proof Theoretical Foundation. CALCO 2009: 127-144 - [c73]Dorel Lucanu, Eugen-Ioan Goriac, Georgiana Caltais, Grigore Rosu:
CIRC: A Behavioral Verification Tool Based on Circular Coinduction. CALCO 2009: 433-442 - [c72]Dorel Lucanu, Grigore Rosu:
Circular Coinduction with Special Contexts. ICFEM 2009: 639-659 - [c71]Feng Chen, Patrick O'Neil Meredith, Dongyun Jin, Grigore Rosu:
Efficient Formalism-Independent Monitoring of Parametric Properties. ASE 2009: 383-394 - [c70]Grigore Rosu, Wolfram Schulte, Traian-Florin Serbanuta:
Runtime Verification of C Memory Safety. RV 2009: 132-151 - [c69]Feng Chen, Grigore Rosu:
Parametric Trace Slicing and Monitoring. TACAS 2009: 246-261 - [e4]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
- [j33]Dorel Lucanu, Grigore Rosu, Gheorghe Grigoras:
Regular Strategies as Proof Tactics for CIRC. Electron. Notes Theor. Comput. Sci. 204: 83-98 (2008) - [c68]