Difference between revisions of "Grigore Rosu's Publications"
From FSL
Line 4: | Line 4: | ||
This list contains only my newer publications. See [http://www.informatik.uni-trier.de/~ley/db/indices/a-tree/r/Rosu:Grigore.html DBLP] and [http://fsl.cs.uiuc.edu/~grosu/publications.html my old publication page] for the remaining papers. | This list contains only my newer publications. See [http://www.informatik.uni-trier.de/~ley/db/indices/a-tree/r/Rosu:Grigore.html DBLP] and [http://fsl.cs.uiuc.edu/~grosu/publications.html my old publication page] for the remaining papers. | ||
<purge></purge> | <purge></purge> | ||
+ | |||
+ | {{Header | 2018}} | ||
+ | |||
+ | <pubbib authors="Grigore Rosu" year="2018" template="grigorePubs"/> | ||
{{Header | 2017}} | {{Header | 2017}} |
Revision as of 10:15, 16 September 2018
(back to Grigore Rosu's page)
This list contains only my newer publications. See DBLP and my old publication page for the remaining papers.
2018 |
---|
- A Language-Independent Program Verification Framework
Xiaohong Chen and Grigore Rosu
ISoLA'18, Springer, pp 92-102. 2018
PDF, Slides(PPTX), DOI, ISoLA'18, BIB
- A Language-Independent Approach to Smart Contract Verification
Xiaohong Chen and Daejun Park and Grigore Rosu
ISoLA'18, Springer, pp 405-413. 2018
PDF, Slides(PPTX), Formally Verified Smart Contracts, DOI, ISoLA'18, BIB
- A Formal Verification Tool for Ethereum VM Bytecode
Daejun Park and Yi Zhang and Manasvi Saxena and Philip Daian and Grigore Rosu
ESEC/FSE'18, ACM, pp 912-915. 2018
PDF, Slides(PDF), Formally Verified Smart Contracts, DOI, ESEC/FSE'18, BIB
- IELE: An Intermediate-Level Blockchain Language Designed and Implemented Using Formal Semantics
Theodoros Kasampalis and Dwight Guth and Brandon Moore and Traian Serbanuta and Virgil Serbanuta and Daniele Filaretti and Grigore Rosu and Ralph Johnson
Technical Report http://hdl.handle.net/2142/100320, July 2018
PDF, IELE, DOI, BIB
- Program Verification by Coinduction
Brandon Moore and Lucas Pena and Grigore Rosu
ESOP'18, Springer, pp 589-618. 2018
PDF, Matching Logic, DOI, ESOP'18, BIB
- P4K: A Formal Semantics of P4 and Applications
Ali Kheradmand and Grigore Rosu
Technical Report https://arxiv.org/abs/1804.01468, April 2018
PDF, P4K, DOI, BIB
- KEVM: A Complete Semantics of the Ethereum Virtual Machine
Everett Hildenbrandt and Manasvi Saxena and Xiaoran Zhu and Nishant Rodrigues and Philip Daian and Dwight Guth and Brandon Moore and Yi Zhang and Daejun Park and Andrei Stefanescu and Grigore Rosu
CSF 2018, IEEE, pp 204-217. 2018
PDF, KEVM, CSF 2018, BIB
2017 |
---|
- Matching logic
Grigore Rosu
LMCS, Volume 13(4), pp 1-61. 2017
PDF, project, DOI, LMCS, BIB
- Open Problems and Challenges 2017
Grigore Rosu
Technical Report http://hdl.handle.net/2142/95775, March 2017
PDF, Webpage, DOI, BIB
- K - A Semantic Framework for Programming Languages and Formal Analysis Tools
Grigore Rosu
Marktoberdorf'16, NATO Science for Peace and Security. 2017. To appear
PDF, K, BIB
2016 |
---|
- Semantics-Based Program Verifiers for All Languages
Andrei Stefanescu and Daejun Park and Shijiao Yuwen and Yilong Li and Grigore Rosu
OOPSLA'16, ACM, pp 74-91. 2016
PDF, Slides(PDF), Matching Logic, DOI, OOPSLA'16, BIB
- Finite-Trace Linear Temporal Logic: Coinductive Completeness
Grigore Rosu
RV'16, LNCS 10012, pp 333-350. 2016
PDF, Slides(PPTX), Matching Logic, DOI, RV'16, BIB
- Runtime Verification at Work: A Tutorial
Philip Daian and Dwight Guth and Chris Hathhorn and Yilong Li and Edgar Pek and Manasvi Saxena and Traian Florin Serbanuta and Grigore Rosu
RV'16, LNCS 10012, pp 46-67. 2016
PDF, Slides(PPTX), RV Products, DOI, RV'16, BIB
- How Good are the Specs? A Study of the Bug-Finding Effectiveness of Existing Java API Specifications
Owolabi Legunsen and Wajih Ul Hassan and Xinyue Xu and Grigore Rosu and Darko Marinov
ASE 2016, IEEE/ACM, pp 602-613. 2016
PDF, Slides(PDF), JavaMOP, DOI, ASE 2016, BIB
- RV-Match: Practical Semantics-Based Program Analysis
Dwight Guth and Chris Hathhorn and Manasvi Saxena and Grigore Rosu
CAV'16, LNCS 9779, pp 447-453. 2016
PDF, RV-Match, DOI, CAV'16, BIB
- A Language-Independent Proof System for Full Program Equivalence
Stefan Ciobaca and Dorel Lucanu and Vlad Rusu and Grigore Rosu
J.FAOC, Volume 28(3), pp 469-497. 2016
PDF, Matching Logic, DOI, J.FAOC, BIB
- RV-ECU: Maximum Assurance In-Vehicle Safety Monitoring
Philip Daian and Bhargava Manja and Shinichi Shiraishi and Akihito Iwai and Grigore Rosu
SAE'16, SAE International 2016-01-0126, pp 1-13. 2016
PDF, Slides(PPT), RV-ECU, DOI, SAE'16, BIB
- Open Problems and Challenges 2016
Grigore Rosu
Technical Report http://hdl.handle.net/2142/88925, February 2016
PDF, Webpage, DOI, BIB
- Language Definitions as Rewrite Theories
Vlad Rusu and Dorel Lucanu and Traian Florin Serbanuta and Andrei Arusoaie and Andrei Stefanescu and Grigore Rosu
J.LAMP, Volume 85(1, Part 1), pp 98-120. 2016
PDF, project, DOI, J.LAMP, BIB
- Towards a Kool Future
Dorel Lucanu and Traian Florin Serbanuta and Grigore Rosu
Boer's Festschrift, LNCS 9660, pp 325-343. 2016
PDF, K, DOI, Boer's Festschrift, BIB
2015 |
---|
- From Rewriting Logic, to Programming Language Semantics, to Program Verification
Grigore Rosu
Meseguer's Festschrift, LNCS 9200, pp 598-616. 2015
PDF, Slides(PPTX), K, DOI, Meseguer's Festschrift, BIB
- RV-Android: Efficient Parametric Android Runtime Verification, a Brief Tutorial
Philip Daian and Ylies Falcone and Patrick Meredith and Traian Florin Serbanuta and Shinichi Shiraishi and Akihito Iwai and Grigore Rosu
RV'15, Lecture Notes in Computer Science 9333, pp 342-357. 2015
PDF, Slides(PDF), RV-Android, DOI, RV'15, BIB
- Matching Logic --- Extended Abstract
Grigore Rosu
RTA'15, Leibniz International Proceedings in Informatics (LIPIcs) 36, pp 5-21. 2015
PDF, Slides(PPTX), Matching Logic, DOI, RTA'15, BIB
- Defining the Undefinedness of C
Chris Hathhorn and Chucky Ellison and Grigore Rosu
PLDI'15, ACM, pp 336-345. 2015
PDF, C Semantics, DOI, PLDI'15, BIB
- KJS: A Complete Formal Semantics of JavaScript
Daejun Park and Andrei Stefanescu and Grigore Rosu
PLDI'15, ACM, pp 346-356. 2015
PDF, Slides(PDF), Semantics, DOI, PLDI'15, BIB
- GPredict: Generic Predictive Concurrency Analysis
Jeff Huang and Qingzhou Luo and Grigore Rosu
ICSE'15, ACM, pp 847-857. 2015
PDF, Slides(PDF), jPredictor, DOI, ICSE'15, BIB
- Evolution-Aware Monitoring-Oriented Programming
Owolabi Legunsen and Darko Marinov and Grigore Rosu
ICSE NIER'15, ACM, pp 615-618. 2015
PDF, Slides(PDF), JavaMOP, DOI, ICSE NIER'15, BIB
- Term-Generic Logic
Andrei Popescu and Grigore Rosu
Journal of Theoretical Computer Science, Volume 577(1), pp 1-24. 2015
PDF, project, DOI, Journal of Theoretical Computer Science, BIB
- Program Verification by Coinduction
Brandon Moore and Grigore Rosu
Technical Report http://hdl.handle.net/2142/73177, February 2015
PDF, Matching Logic, DOI, BIB
- K-Java: A Complete Semantics of Java
Denis Bogdanas and Grigore Rosu
POPL'15, ACM, pp 445-456. 2015
PDF, Slides(PDF), K-Java, DOI, POPL'15, BIB
2014 |
---|
- A Language-Independent Proof System for Mutual Program Equivalence
Stefan Ciobaca and Dorel Lucanu and Vlad Rusu and Grigore Rosu
ICFEM'14, LNCS 8829, pp 75-90. 2014
PDF, Slides(PDF), Matching Logic, DOI, ICFEM'14, BIB
- ROSRV: Runtime Verification for Robots
Jeff Huang and Cansu Erdogan and Yi Zhang and Brandon Moore and Qingzhou Luo and Aravind Sundaresan and Grigore Rosu
RV'14, LNCS 8734, pp 247-254. 2014
PDF, Slides(PPTX), Slides(PDF), ROSRV, DOI, RV'14, BIB
- RV-Monitor: Efficient Parametric Runtime Verification with Simultaneous Properties
Qingzhou Luo and Yi Zhang and Choonghwan Lee and Dongyun Jin and Patrick O'Neil Meredith and Traian Florin Serbanuta and Grigore Rosu
RV'14, LNCS 8734, pp 285-300. 2014
PDF, Slides(PPTX), JavaMOP, DOI, RV'14, BIB
- All-Path Reachability Logic
Andrei Stefanescu and Stefan Ciobaca and Radu Mereuta and Brandon Moore and Traian Florin Serbanuta and Grigore Rosu
RTA'14, LNCS 8560, pp 425-440. 2014
PDF, Slides(PPTX), Matching Logic, DOI, RTA'14, BIB
- Maximal Sound Predictive Race Detection with Control Flow Abstraction
Jeff Huang and Patrick Meredith and Grigore Rosu
PLDI'14, ACM, pp 337-348. 2014
PDF, Slides(PPT), Slides(PDF), jPredictor, DOI, PLDI'14, BIB
- On the Complexity of Stream Equality
Joerg Endrullis and Dimitri Hendriks and Rena Bakhshi and Grigore Rosu
Journal of Functional Programming, Volume 24(2-3), pp 166-217. 2014
PDF, CIRC, DOI, Journal of Functional Programming, BIB
- Language Definitions as Rewrite Theories
Andrei Arusoaie and Dorel Lucanu and Vlad Rusu and Traian Florin Serbanuta and Andrei Stefanescu and Grigore Rosu
WRLA'14, LNCS 8663, pp 97-112. 2014
PDF, K, DOI, WRLA'14, BIB
- Behavioral Rewrite Systems and Behavioral Productivity
Grigore Rosu and Dorel Lucanu
Futatsugi Festschrift 2014, LNCS 8373, pp 296-314. 2014
PDF, Slides(PPTX), CIRC, DOI, Futatsugi Festschrift 2014, BIB
- Matching Logic: A Logic for Structural Reasoning
Grigore Rosu
Technical Report http://hdl.handle.net/2142/47004, Jan 2014
PDF, Matching Logic, DOI, BIB
2013 |
---|
- K Overview and SIMPLE Case Study
Grigore Rosu and Traian Florin Serbanuta
K'11, ENTCS 304, pp 3-56. 2014
PDF, K, DOI, K'11, BIB
- Abstract Semantics for K Module Composition
Codruta Girlea and Grigore Rosu
K'11, ENTCS 304, pp 127-149. 2014
PDF, K, DOI, K'11, BIB
- The K Primer (version 3.3)
Traian Florin Serbanuta and Andrei Arusoaie and David Lazar and Chucky Ellison and Dorel Lucanu and Grigore Rosu
K'11, ENTCS 304, pp 57-80. 2014
PDF, K, DOI, K'11, BIB
- The Rewriting Logic Semantics Project: A Progress Report
Jose Meseguer and Grigore Rosu
Information and Computation, Volume 231(1), pp 38-69. 2013
PDF, K, DOI, Information and Computation, BIB
- Specifying Languages and Verifying Programs with K
Grigore Rosu
SYNASC'13, IEEE/CPS, pp 28-31. 2013
PDF, Slides(PPTX), K, DOI, SYNASC'13, BIB
- EnforceMOP: A Runtime Property Enforcement System for Multithreaded Programs
Qingzhou Luo and Grigore Rosu
ISSTA'13, ACM, pp 156-166. 2013
PDF, Slides(PPTX), EnforceMOP, DOI, ISSTA'13, BIB
- One-Path Reachability Logic
Grigore Rosu and Andrei Stefanescu and Stefan Ciobaca and Brandon Moore
LICS'13, IEEE, pp 358-367. 2013
PDF, Slides(PPTX), Reachability Logic, LICS'13, BIB
- Low-Level Program Verification using Matching Logic Reachability
Dwight Guth and Andrei Stefanescu and Grigore Rosu
LOLA'13. 2013
PDF, Slides(PDF), Matching Logic, LOLA'13, BIB
- Efficient Parametric Runtime Verification with Deterministic String Rewriting
Patrick Meredith and Grigore Rosu
ASE'13, IEEE/ACM, pp 70-80. 2013
PDF, Slides(PPT), Slides(KEY), Slides(PDF), MOP, DOI, ASE'13, BIB
2012 |
---|
- A Truly Concurrent Semantics for the K Framework Based on Graph Transformations
Traian Florin Serbanuta and Grigore Rosu
ICGT'12, LNCS 7562, pp 294-310. 2012
PDF, ICGT'12, Slides(PDF), BIB
- Maximal Causal Models for Sequentially Consistent Systems
Traian Florin Serbanuta, Feng Chen and Grigore Rosu
RV'12, LNCS. 7687, pp 136-150. 2013
PDF, Slides(PDF), BIB
- Checking Reachability using Matching Logic
Grigore Rosu and Andrei Stefanescu
OOPSLA'12, ACM, pp 555-574. 2012
PDF, Slides(pptx), Slides(pdf), Matching Logic, OOPSLA'12, BIB
- Reachability Logic
Grigore Rosu, Andrei Stefanescu, Stefan Ciobaca and Brandon Moore
Technical Report http://hdl.handle.net/2142/32952, July 2012
PDF, TR@UIUC
- From Hoare Logic to Matching Logic Reachability
Grigore Rosu and Andrei Stefanescu
FM'12, LNCS 7436, pp 387-402. 2012
PDF, Slides(pptx), Slides(pdf), Matching Logic, FM'12, , BIB
- Security-Policy Monitoring and Enforcement with JavaMOP
Soha Hussein, Patrick Meredith and Grigore Rosu
PLAS'12, ACM, pp 3:1-3:11. 2012
PDF, Slides(KEY), Slides(PDF), ACM, PLAS'12, BIB
- Executing Formal Semantics with the K Tool
David Lazar, Andrei Arusoaie, Traian Florin Serbanuta, Chucky Ellison, Radu Mereuta, Dorel Lucanu and Grigore Rosu
FM'12, LNCS 7436, pp 267-271. 2012
PDF, Slides(PDF), FM'12, DBLP, BIB
- Towards a Unified Theory of Operational and Axiomatic Semantics
Grigore Rosu and Andrei Stefanescu
ICALP'12, LNCS 7392, pp 351-363. 2012
PDF, Slides(pptx), Slides(pdf), Matching Logic, ICALP'12, BIB
- Defining the Undefinedness of C
Chucky Ellison and Grigore Rosu
Technical Report http://hdl.handle.net/2142/30780, April 2012
PDF, TR@UIUC, BIB
- Scalable Parametric Runtime Monitoring
Dongyun Jin, Patrick Meredith and Grigore Rosu
Technical Report http://hdl.handle.net/2142/30757, April 2012
PDF, TR@UIUC, BIB
- Efficient Parametric Runtime Verification with Deterministic String Rewriting
Patrick Meredith and Grigore Rosu
Technical Report http://www.ideals.illinois.edu/handle/2142/30467, March 2012
PDF, TR@UIUC, BIB
- K Framework Distilled
Dorel Lucanu, Traian Florin Serbanuta and Grigore Rosu
WRLA'12, LNCS 7571, pp 31-53. 2012 Invited Paper
PDF, Slides (PDF), WRLA'12, LNCS, BIB
- JavaMOP: Efficient Parametric Runtime Monitoring Framework
Dongyun Jin, Patrick Meredith, Choonghwan Lee and Grigore Rosu
ICSE'12, IEEE, pp 1427-1430. 2012
PDF, Demo Movie, TOOL ICSE'12, BIB
- Towards Categorizing and Formalizing the JDK API
Choonghwan Lee, Dongyun Jin, Patrick Meredith and Grigore Rosu
Technical Report http://hdl.handle.net/2142/30006, March 2012
PDF, TR@UIUC, BIB
- Semantics and Algorithms for Parametric Monitoring
Grigore Rosu and Feng Chen
J.LMCS, Volume 8(1), pp 1-47. 2012
PDF, MOP, J.LMCS, BIB
- The K Primer (version 2.5)
Traian Florin Serbanuta, Andrei Arusoaie, David Lazar, Chucky Ellison, Dorel Lucanu and Grigore Rosu
Technical Report, January 2012
PDF, K 2.5, BIB
- Making Maude Definitions more Interactive
Andrei Arusoaie, Traian Florin Serbanuta, Chucky Ellison and Grigore Rosu
WRLA'12, LNCS 7571. 2012
PDF, Slides (PDF), WRLA'12, BIB
- An Executable Formal Semantics of C with Applications
Chucky Ellison and Grigore Rosu
POPL'12, ACM, pp 533-544. 2012
PDF, Slides(PDF), Project, ACM, POPL'12, DBLP, BIB
2011 |
---|
- Matching Logic Rewriting: Unifying Operational and Axiomatic Semantics in a Practical and Generic Framework
Grigore Rosu and Andrei Stefanescu
Technical Report http://hdl.handle.net/2142/28357, November 2011
PDF, Matching Logic, TR@UIUC, , BIB
- The Rewriting Logic Semantics Project: A Progress Report
Jose Meseguer and Grigore Rosu
FCT'11, LNCS 6914, pp 1-37. Invited talk. 2011
PDF, K Tool, FCT'11, BIB
- Improved Multithreaded Unit Testing
Vilas Jagannath, Milos Gligoric, Dongyun Jin, Qingzhou Luo, Grigore Rosu and Darko Marinov
FSE'11, ACM, pp 223-233. 2011
PDF, FSE'11, BIB
- Matching Logic: A New Program Verification Approach (NIER Track)
Grigore Rosu and Andrei Stefanescu
ICSE'11, ACM, pp. 868-871. 2011
PDF, Slides(pptx), Slides(pdf), Poster(pptx), Poster(pdf), Matching Logic, ACM, NIER ICSE'11, BIB
- Garbage Collection for Monitoring Parametric Properties
Dongyun Jin, Patrick Meredith, Dennis Griffith and Grigore Rosu
PLDI'11, ACM, pp 415-424. 2011
PDF, PLDI'11 slides(pptx), PLDI'11 slides(pdf), ACM, PLDI'11, JavaMOP, BIB
- Mining Parametric Specifications
Choonghwan Lee, Feng Chen and Grigore Rosu
ICSE'11, ACM, pp 591-600. 2011
PDF, Slides(pptx), ACM, ICSE'11, jMiner, BIB
- An Overview of the MOP Runtime Verification Framework
Patrick Meredith, Dongyun Jin, Dennis Griffith, Feng Chen and Grigore Rosu
J.STTT, http://dx.doi.org/10.1007/s10009-011-0198-6
PDF, J.STTT, BIB
- Maximal Causal Models for Sequentially Consistent Systems
Traian Florin Serbanuta and Feng Chen and Grigore Rosu
Technical Report http://hdl.handle.net/2142/27708, October 2011
PDF, JPredictor, DOI, BIB
- Improved Multithreaded Unit Testing
Vilas Jagannath and Milos Gligoric and Dongyun Jin and Qingzhou Luo and Grigore Rosu and Darko Marinov
FSE'11, ACM, pp 223-233. 2011
PDF, DOI, FSE'11, BIB
- The Rewriting Logic Semantics Project: A Progress Report
Jose Meseguer and Grigore Rosu
FCT'11, Lecture Notes in Computer Science 6914, pp 1-37. 2011
PDF, K, DOI, FCT'11, BIB
- An Executable Formal Semantics of C with Applications
Chucky Ellison and Grigore Rosu
Technical Report http://hdl.handle.net/2142/25816, July 2011
PDF, C Semantics, DOI, BIB
- Towards Semantics-Based WCET Analysis
Mihail Asavoae and Dorel Lucanu and Grigore Rosu
WCET'11. 2011
PDF, Slides(PDF), Matching Logic, WCET'11, BIB
- Garbage Collection for Monitoring Parametric Properties
Dongyun Jin and Patrick O'Neil Meredith and Dennis Griffith and Grigore Rosu
PLDI'11, ACM, pp 415-424. 2011
PDF, Slides(PPTX), Slides(PDF), MOP, DOI, PLDI'11, BIB
- An Overview of the MOP Runtime Verification Framework
Patrick O'Neil Meredith and Dongyun Jin and Dennis Griffith and Feng Chen and Grigore Rosu
J.STTT, Volume 14(3), pp 249-289. 2011
PDF, MOP, DOI, J.STTT, BIB
- Matching Logic: A New Program Verification Approach (NIER Track)
Grigore Rosu and Andrei Stefanescu
ICSE'11, ACM, pp 868-871. 2011
PDF, Slides(PPTX), Slides(PDF), Matching Logic, DOI, ICSE'11, BIB
- Mining Parametric Specifications
Choonghwan Lee and Feng Chen and Grigore Rosu
ICSE'11, ACM, pp 591-600. 2011
PDF, Slides(PPTX), JMiner, DOI, ICSE'11, BIB
2010 |
---|
- On Compiling Rewriting Logic Language Definitions into Competitive Interpreters
Michael Ilseman, Chucky Ellison and Grigore Rosu
Technical Report http://hdl.handle.net/2142/17444, December 2010
PDF, TR@UIUC, Compiler Webpage, BIB
- Matching Logic: A New Program Verification Approach
Grigore Rosu and Andrei Stefanescu
UV'10. 2010
PDF, Slides(pptx), Slides(pdf), Matching Logic, K framework, UV'10, BIB
- Runtime Verification with the RV System
Patrick Meredith and Grigore Rosu
RV'10, LNCS 6418, pp 136-152. 2010
PDF, Slides(PDF), Slides(PPT), Slides(KEY), RV'10, BIB
- Automating Coinduction with Case Analysis
Eugen-Ioan Goriac, Dorel Lucanu and Grigore Rosu
ICFEM'10, LNCS 6447, pp 220-236. 2010
PDF, LNCS, ICFEM'10, CIRC, BIB
- A Formal Executable Semantics of Verilog
Patrick Meredith, Michael Katelman, Jose Meseguer and Grigore Rosu
Technical Report http://hdl.handle.net/2142/17079, July 2010
PDF, TR@UIUC, BIB
- Matching Logic: An Alternative to Hoare/Floyd Logic
Grigore Rosu, Chucky Ellison and Wolfram Schulte
AMAST'10, LNCS 6486, pp 142-162. 2010
PDF, Slides(PPT), Slides(PDF), LNCS, AMAST'10, BIB
- K-Maude: A Rewriting Based Tool for Semantics of Programming Languages
Traian Florin Serbanuta and Grigore Rosu
WRLA'10, LNCS 6381, pp 104-122. 2010
PDF, Slides (PDF), K-Maude, LNCS, WRLA'10, BIB
- An Overview of the K Semantic Framework
Grigore Rosu and Traian Florin Serbanuta
J.LAP, Volume 79(6), pp 397-434. 2010
PDF, Slides(PPTX), Slides(PDF), K Tool, J.LAP, BIB
- A Formal Executable Semantics of Verilog
Patrick Meredith, Michael Katelman, Jose Meseguer and Grigore Rosu
MEMOCODE'10, IEEE, pp 179-188. 2010
PDF, Slides(PDF), Sources, Verilog Semantics, IEEE, MEMOCODE'10, BIB
- IMUnit: Improved Multithreaded Unit Testing
Vilas Jagannath, Milos Gligoric, Dongyun Jin, Grigore Rosu and Darko Marinov
IWMSE'10, IEEE, pp 48-49. 2010
PDF, IEEE, IWMSE'10, BIB
- Efficient Monitoring of Parametric Context-Free Patterns
Patrick Meredith, Dongyun Jin, Feng Chen and Grigore Rosu
J. of ASE, Volume 17(2), pp 149-180. 2010
PDF, J.ASE, BIB
2009 |
---|
- Efficient Formalism-Independent Monitoring of Parametric Properties
Feng Chen, Patrick Meredith, Dongyun Jin and Grigore Rosu
ASE'09, IEEE/ACM, pp 383-394. 2009
PDF, ASE'09 slides(KEY), ASE'09 slides(PDF), IEEE, ASE'09, BIB
- Circular Coinduction with Special Contexts
Dorel Lucanu and Grigore Rosu
ICFEM'09, LNCS 5885, pp 639-659. 2009
PDF, Slides(PDF), LNCS, ICFEM'09, BIB
- A Rewriting Logic Approach to Type Inference
Chucky Ellison, Traian Florin Serbanuta and Grigore Rosu
WADT'08, LNCS 5486, pp 135-151. 2009
PDF, Slides(PDF), LNCS, WADT'08, BIB
- Runtime Verification of C Memory Safety
Grigore Rosu, Wolfram Schulte and Traian Florin Serbanuta
RV'09, LNCS 5779, pp 132-151. 2009
PDF, Slides (PDF), LNCS, RV'09, BIB
- Circular Coinduction: A Proof Theoretical Foundation
Grigore Rosu and Dorel Lucanu
CALCO'09, LNCS 5728, pp 127-144. 2009
Slides (PDF), LNCS, CALCO'09, DBLP, BIB
- From Rewriting Logic Executable Semantics to Matching Logic Program Verification
Grigore Rosu, Chucky Ellison and Wolfram Schulte
Technical Report http://hdl.handle.net/2142/13159, July 2009
PDF, TR@UIUC, BIB
- Matching Logic --- Extended Report
Grigore Rosu and Wolfram Schulte
Technical Report UIUCDCS-R-2009-3026, January 2009
TR@UIUC, BIB
- A Semantic Approach to Interpolation
Andrei Popescu, Traian Florin Serbanuta and Grigore Rosu
J. of TCS, Volume 410(12-13), pp 1109-1128. 2009
PDF, J.TCS, BIB
- Monitoring Oriented Programming - A Project Overview
Feng Chen, Dongyun Jin, Patrick Meredith, and Grigore Rosu
ICICIS'09, pp 72-77. 2009
PDF, ICICIS'09, BIB
- A Rewriting Logic Approach to Operational Semantics
Traian Florin Serbanuta, Grigore Rosu and Jose Meseguer
Information and Computation, Volume 207(2), pp 305-340. 2009
PDF, Experiments, J.Inf.&Comp., BIB
- Parametric Trace Slicing and Monitoring
Feng Chen and Grigore Rosu
TACAS'09, LNCS 5505, pp 246-261. 2009.
PDF, Slides (PPT), LNCS, TACAS'09, DBLP, BIB
- Dependent advice: A general approach to optimizing history-based Aspects
Eric Bodden, Feng Chen and Grigore Rosu
AOSD'09, ACM, pp 3--14. 2009.
PDF, ACM, AOSD'09, TR@ABC, BIB
2008 |
---|
- Towards a Module System for K
Mark Hills and Grigore Rosu
WADT'08, LNCS 5486, pp 187-205. 2009
PDF, LNCS, WADT'08, BIB
- Term-Generic Logic
Andrei Popescu and Grigore Rosu
WADT'08, LNCS 5486, pp 290-307. 2009
LNCS, WADT'08, BIB
- Hardware Runtime Monitoring for Dependable COTS-based Real-Time Embedded Systems
Rodolfo Pellizzoni, Patrick Meredith, Marco Caccamo and Grigore Rosu
RTSS'08, IEEE, pp. 481-491. 2008
PDF, Experiments, Slides(PPTX), IEEE, RTSS'08, BIB
- Defining and Executing P-systems with Structured Data in K
Traian Florin Serbanuta, Gheorghe Stefanescu and Grigore Rosu
WMC'08, LNCS 5391, pp 374-393. 2009
PDF, Slides (PDF), Experiments, LNCS, WMC'08, BIB
- Efficient Monitoring of Parametric Context-Free Patterns
Patrick Meredith, Dongyun Jin, Feng Chen and Grigore Rosu
ASE'08, IEEE/ACM, pp 148-157. 2008 ACM Sigsoft Distinguished Paper
PDF, Experiments, ASE'08 slides(KEY), ASE'08 slides(MOV), ASE'08 slides(PPT), IEEE, ASE'08, BIB
- Mining Parametric State-Based Specifications from Executions
Feng Chen and Grigore Rosu
Technical report UIUCDCS-R-2008-3000, September 2008
PDF, BIB
- A Rewriting Logic Approach to Static Checking of Units of Measurement in C
Mark Hills, Feng Chen and Grigore Rosu
RULE'08, ENTCS, to appear, 2008
PDF, RULE'08 slides, RULE'08, BIB
- Monitoring IVHM Systems using a Monitor-Oriented Programming Framework
Sudipto Ghoshal, Solaiappan Manimaran, Grigore Rosu, Traian Florin Serbanuta, and Gheorghe Stefanescu
LFM 2008
PDF, Slides (PPT), LFM'08, BIB
- jPredictor: A Predictive Runtime Analysis Tool for Java
Feng Chen and Traian Florin Serbanuta and Grigore Rosu
ICSE'08, ACM, pp. 221-230. 2008
PDF, Slides(PDF), DOI, ICSE'08, BIB
- A Rewriting Logic Approach to Type Inference
Chucky Ellison, Traian Florin Serbanuta and Grigore Rosu
Technical report UIUCDCS-R-2008-2934, March 2008
PDF, TR@UIUC, BIB
- Synthesizing Monitors for Safety Properties -- This Time With Calls and Returns --
Grigore Rosu, Feng Chen and Thomas Ball
RV'08, LNCS 5289, pp 51-68, 2008
PDF, RV'08, BIB
- Pluggable Policies for C
Mark Hills, Feng Chen and Grigore Rosu
Technical Report UIUCDCS-R-2008-2931, January 2008
PDF, TR@UIUC, BIB
2007 |
---|
- K: A Rewriting-Based Framework for Computations -- Preliminary version
Grigore Rosu
Technical report UIUCDCS-R-2007-2926 and UILU-ENG-2007-1827, December 2007
PDF, ZIP, TR@UIUC, BIB
- Synthesizing Monitors for Safety Properties -- This Time With Calls and Returns --
Grigore Rosu,Feng Chen and Thomas Ball
Technical report UIUCDCS-R-2007-2908, October 2007
PDF, BIB
- A K Definition of Scheme
Patrick Meredith, Mark Hills and Grigore Rosu
Technical Report UIUCDCS-R-2007-2907, October 2007
PDF, TR@UIUC, BIB
- Effective Predictive Runtime Analysis Using Sliced Causality and Atomicity
Feng Chen, Traian Florin Serbanuta and Grigore Rosu
Technical report UIUCDCS-R-2007-2905, October 2007
PDF, TR@UIUC, BIB
- An Executable Rewriting Logic Semantics of K-Scheme
Patrick Meredith, Mark Hills and Grigore Rosu
8th Workshop on Scheme and Functional Programming, Technical Report DIUL-RT-0701, pp. 91-103, September 2007
PDF, SCHEME'07, BIB
- A Rewriting Approach to the Design and Evolution of Object-Oriented Languages
Mark Hills and Grigore Rosu
OOPSLA'07 Companion, ACM Press, pp 827-828. 2007
PDF, OOPSLA'07 poster, ACM, OOPSLA'07, BIB
- A Rewriting Approach to the Design and Evolution of Object-Oriented Languages
Mark Hills and Grigore Rosu
Technical Report Bericht-Nr. 2007-7, pp. 23-26, July 2007
PDF, ECOOP'07 Doctoral Symposium slides, ECOOP'07 Doctoral Symposium, BIB
- MOP: An Efficient and Generic Runtime Verification Framework
Feng Chen and Grigore Rosu
OOPSLA'07, ACM press, pp 569-588. 2007
PDF, OOPSLA'07 slides, ACM, OOPSLA'07, DBLP, TR@UIUC, BIB
- A Rewriting Logic Approach to Operational Semantics -- Extended Abstract
Traian Florin Serbanuta, Grigore Rosu and Jose Meseguer
SOS'07, ENTCS 192(1), pp 125-141. 2007
PDF, Slides (PPT), ENTCS, SOS'07, BIB
- CIRC: A Circular Coinductive Prover
Dorel Lucanu and Grigore Rosu
CALCO'07, LNCS 4624, pp 372-378. 2007
PDF, CIRC webpage, CALCO'07, BIB
- Parametric and Sliced Causality
Feng Chen and Grigore Rosu
CAV'07, LNCS 4590, pp 240 - 253, 2007
PDF, CAV'07 slides, CAV'07, TR@UIUC, BIB
- On Formal Analysis of OO Languages using Rewriting Logic: Designing for Performance
Mark Hills and Grigore Rosu
FMOODS'07, LNCS 4468, pp 107-121. 2007
PDF, FMOODS'07 slides, LNCS, FMOODS'07, BIB
- KOOL: An Application of Rewriting Logic to Language Prototyping and Analysis
Mark Hills and Grigore Rosu
RTA'07, LNCS 4533, pp 246-256. 2007
PDF, RTA'07 slides, LNCS, RTA'07, BIB
- On Safety Properties and Their Monitoring
Grigore Rosu
Technical report UIUCDCS-R-2007-2850, February 2007
PDF, ZIP, TR@UIUC, BIB
- An Effective Algorithm for the Membership Problem for Extended Regular Expressions
Grigore Rosu
FOSSACS'07, LNCS 4423, pp 332-345, 2007
PDF, FOSSACS'07, BIB
- The Rewriting Logic Semantics Project
Jose Meseguer and Grigore Rosu
J. of TCS, Volume 373(3), pp 213-237. 2007
PDF, J.TCS, BIB
2006 |
---|
- A Rewrite Framework for Language Definitions and for Generation of Efficient Interpreters
Mark Hills, Traian Florin Serbanuta and Grigore Rosu
WRLA'06, ENTCS 176(4), pp. 215-231. 2007
PDF, Experiments, ENTCS, WRLA'06, BIB
- K: a Rewrite-based Framework for Modular Language Design, Semantics, Analysis and Implementation
Grigore Rosu
Technical report UIUCDCS-R-2006-2802, December 2006
PDF, TR@UIUC, BIB
- A Rewriting Based Approach to OO Language Prototyping and Design
Mark Hills and Grigore Rosu
Technical Report UIUCDCS-R-2006-2786, October 2006
PDF, TR@UIUC, BIB
- KOOL: A K-based Object-Oriented Language
Mark Hills and Grigore Rosu
Technical Report UIUCDCS-R-2006-2779, October 2006
PDF, TR@UIUC, BIB
- MOP: Reliable Software Development using Abstract Aspects
Feng Chen and Grigore Rosu
Technical report UIUCDCS-R-2006-2776, October 2006
PDF, TR@UIUC, BIB
- Computationally Equivalent Elimination of Conditions - extended abstract
Traian Florin Serbanuta and Grigore Rosu
RTA'06, LNCS 4098, pp 19-34. 2006
PDF, Slides (PPT), Experiments, LNCS, RTA'06, DBLP, BIB
- GFOL: a Term-Generic Logic for Defining Lambda-Calculi
Andrei Popescu and Grigore Rosu
Technical Report UIUCDCS-R-2006-2756, July 2006
PDF, TR@UIUC, BIB
- Equality of Streams is a Pi_2^0-Complete Problem
Grigore Rosu
ICFP'06, ACM, 2006
PDF, ICFP'06 Slides, ACM, ICFP'06, BIB
- Complete Categorical Deduction for Satisfaction as Injectivity
Grigore Rosu
Festschrift in Honor of Joseph Goguen, LNCS 4060, pp 157-172. 2006.
PDF, Goguen's Festschrift slides, LNCS, Goguen's Festschrift, Goguen's Webpage, BIB
- Allen Linear (Interval) Temporal Logic -Translation to LTL and Monitor Synthesis-
Grigore Rosu and Saddek Bensalem
CAV'06, LNCS 4144, pp 263-277, 2006
PDF, CAV'06, CAV'06 Slides, BIB
- Parametric and Termination-Sensitive Control Dependence - Extended Abstract
Feng Chen and Grigore Rosu
SAS'06, LNCS 4134, pp 387-404. 2006.
PDF, LNCS, SAS'06, BIB
- Parametric and Termination-Sensitive Control Dependence
Feng Chen and Grigore Rosu
Technical report UIUCDCS-R-2006-2712, April 2006
PDF, TR@UIUC, BIB
- A Rewrite Logic Approach to Semantic Definition, Design and Analysis of Object-Oriented Languages
Feng Chen, Mark Hills and Grigore Rosu
Technical Report UIUCDCS-R-2006-2702, March 2006
PDF, TR@UIUC, BIB
- Predicting Concurrency Errors at Runtime using Sliced Causality
Feng Chen and Grigore Rosu
Technical report UIUCDCS-R-2006-2965, 2006.
PDF, TR@UIUC, BIB
- A Semantic Approach to Interpolation
Andrei Popescu, Traian Florin Serbanuta and Grigore Rosu
FOSSACS'06, LNCS 3921, pp 307-321. 2006
PDF, Slides (PDF), LNCS, FOSSACS '06, DBLP, BIB
- Static Analysis to Enforce Safe Value Flow in Embedded Control Systems
Sumant Kowshik, Grigore Rosu and Lui Sha
DSN'06, IEEE, pp 23-34. 2006.
PDF, DSN'06 Slides, IEEE, DSN'06, BIB
2005 |
---|
- Efficient Monitoring of Omega-Languages
Marcelo d'Amorim and Grigore Rosu
CAV'05, LNCS 3576, pp 364 - 378. 2005.
PDF, LNCS, CAV'05, DBLP, BIB
- Behavioral Extensions of Institutions
Andrei Popescu and Grigore Rosu
CALCO'05, LNCS 3629, pp. 331-347. 2005
PDF, CALCO'05 Slides, LNCS , CALCO '05, DBLP, BIB
- Predicting Concurrency Errors at Runtime using Sliced Causality
Feng Chen and Grigore Rosu
Technical report UIUCDCS-R-2005-2660, 2005.
PDF, TR@UIUC, BIB
- Checking and Correcting Behaviors of Java Programs at Runtime with Java-MOP
Feng Chen, Marcelo d'Amorim and Grigore Rosu
RV'05, ENTCS 144, issue 4, pp 3-20. 2005.
PDF, ENTCS, RV'05, DBLP, BIB
- Java-MOP: A Monitoring Oriented Programming Environment for Java
Feng Chen and Grigore Rosu
TACAS'05, LNCS 3440, pp 546-550. 2005.
PDF, LNCS, TACAS'05, DBLP, BIB
- Automatic and Precise Dimensional Analysis
Marcelo d'Amorim, Mark Hills, Feng Chen and Grigore Rosu
Technical Report UIUCDCS-R-2005-2668, December 2005
PDF, Sources, TR@UIUC, BIB
- K: a Rewrite-based Framework for Modular Language Design, Semantics, Analysis and Implementation
Grigore Rosu
Technical Report UIUCDCS-R-2005-2672, December 2005
PDF, Experiments, BIB
- An Executable Semantic Definition of the Beta Language using Rewriting Logic
Mark Hills, T. Baris Aktemur and Grigore Rosu
Technical Report UIUCDCS-R-2005-2650, November 2005
PDF, TR@UIUC, BIB
- Rewriting-based Techniques for Runtime Verification
Grigore Rosu and Klaus Havelund
J.ASE, Volume 12(2), pp 151-197. 2005
PDF, J.ASE, DBLP, BIB
- The Rewriting Logic Semantics Project
Jose Meseguer and Grigore Rosu
SOS'05, ENTCS 156, pp. 27-56. 2006
PDF, SOS'05, BIB
- An Effective Algorithm for the Membership Problem for Extended Regular Expressions
Grigore Rosu
Technical Report UIUCDCS-R-2005-2694, August 2005
PDF, Technical Report @ UIUC, BIB
- Monitoring Algorithms for Metric Temporal Logic
Prasanna Thati and Grigore Rosu
RV'05, Electronic Notes in Theoretical Computer Science 113, pp 145-162. 2005
PDF, MOP, DOI, RV'05, BIB
- Rewriting-Based Techniques for Runtime Verification
Grigore Rosu and Klaus Havelund
J.ASE, Volume 12(2), pp 151-197. 2005
PDF, MOP, DOI, J.ASE, BIB
2004 |
---|
- Rewriting Logic Semantics: From Language Specifications to Formal Analysis Tools
Jose Meseguer and Grigore Rosu
IJCAR'04, LNCS 3097, pp 1-44. 2004
PDF, Maude-code, LNCS, IJCAR'04, BIB
- Efficient Monitoring of Safety Properties
Klaus Havelund and Grigore Rosu
J. of STTT, Volume 6(2), pp 158-173. 2004
PDF, J.STTT, BIB
- A Formal Monitoring-based Framework for Software Development and Analysis
Feng Chen and Marcelo d'Amorim and Grigore Rosu
ICFEM'04, LNCS 3308, pp 357 - 373. 2004.
PDF, LNCS, ICFEM'04, DBLP, BIB
- Monitoring-Oriented Programming: A Tool-Supported Methodology for Higher Quality Object-Oriented Software
Feng Chen, Marcelo d'Amorim and Grigore Rosu
Technical Report UIUCDCS-R-2004-2420, 2004.
PDF, TR@UIUC, BIB
- Formal Analysis of Java Programs in JavaFAN
Azadeh Farzan, Feng Chen, Jose Meseguer and Grigore Rosu
CAV'04, LNCS 3114, pp 501 - 505. 2004.
PDF, LNCS, CAV'04, DBLP, BIB
- From Conditional to Unconditional Rewriting
Grigore Rosu
WADT'04, LNCS 3423, pp 218-233. 2004
PDF, LNCS, WADT'04, Experiments, PDF - Original submission, WADT'04 slides, BIB
- From Conditional to Unconditional Rewriting
Grigore Rosu
Technical Report UIUCDCS-R-2004-2471, August 2004
PDF, Technical reports' page, Experiments, BIB
- Behavioral Abstraction is Hiding Information
Grigore Rosu
J. of TCS, Volume 327(1-2), pp 197-221. 2004
PDF, J.TCS, BIB
2003 |
---|
- Certifying Measurement Unit Safety Policy
Grigore Rosu and Feng Chen
ASE'03, IEEE, pp. 304 - 309. 2003.
PDF, IEEE, ASE'03, BIB
- Rule-Based Analysis of Dimensional Safety
Feng Chen and Grigore Rosu and Ram Prasad Venkatesan
RTA'03, LNCS 2706, pp197 - 207. 2003.
PDF, LNCS, RTA'03, DBLP, BIB
- Towards Monitoring-Oriented Programming: A Paradigm Combining Specification and Implementation
Feng Chen and Grigore Rosu
RV'03, ENTCS 89, issue 2, pp 108 - 127. 2003.
PDF, ENTCS, RV'03, DBLP, BIB
- CS322 - Programming Language Design: Lecture Notes
Grigore Rosu
Technical Report UIUCDCS-R-2003-2897, December 2003
PDF, TR @ UIUC, BIB
- Inductive Behavioral Proofs by Unhiding
Grigore Rosu
CMCS'03, ENTCS 82(1). 2003
PDF, ENTCS, CMCS'03, Experiments, DBLP, BIB
- CS322 - Programming Language Design: Lecture Notes
Grigore Rosu
Technical Report http://hdl.handle.net/2142/11385, December 2003
PDF, Matching Logic, DOI, BIB
- Generating Optimal Linear Temporal Logic Monitors by Coinduction
Koushik Sen and Grigore Rosu and Gul Agha
ASIAN'03, Lecture Notes in Computer Science (LNCS) 2896, pp 260-275. 2003
PDF, MOP, DOI, ASIAN'03, BIB
- Certifying Measurement Unit Safety Policy
Grigore Rosu and Feng Chen
ASE'03, IEEE, pp 304-309. 2003
PDF, MOP, DOI, ASE'03, BIB
- Certifying and Synthesizing Membership Equational Proofs
Grigore Rosu and Steven Eker and Patrick Lincoln and Jose Meseguer
FME'03, Lecture Notes in Computer Science (LNCS) 2805, pp 359-380. 2003
PDF, Slides(PPT), Maude, DOI, FME'03, BIB
- Generating Optimal Monitors for Extended Regular Expressions
Koushik Sen and Grigore Rosu
RV'03, Electronic Notes in Theoretical Computer Science 89(2), pp 226-245. 2003
PDF, MOP, DOI, RV'03, BIB
- Testing Extended Regular Language Membership Incrementally by Rewriting
Grigore Rosu and Mahesh Viswanathan
RTA'03, Lecture Notes in Computer Science (LNCS) 2706, pp 499-514. 2003
PDF, Slides(PPT), MOP, DOI, RTA'03, BIB
- Rule-Based Analysis of Dimensional Safety
Feng Chen and Grigore Rosu and Ram prasad Venkatesan
RTA'03, Lecture Notes in Computer Science (LNCS) 2706, pp 197-207. 2003
PDF, MOP, DOI, RTA'03, BIB
- Towards Monitoring-Oriented Programming: A Paradigm Combining Specification and Implementation
Feng Chen and Grigore Rosu
RV'03, Electronic Notes in Theoretical Computer Science 89(2), pp 108-127. 2003
PDF, MOP, DOI, RV'03, BIB
- Inductive Behavioral Proofs by Unhiding
Grigore Rosu
CMCS'03, Volume 82(1), pp 285-302. 2003
PDF, Logic, DOI, CMCS'03, BIB
2002 |
---|
- Synthesizing Monitors for Safety Properties
Klaus Havelund and Grigore Rosu
TACAS'02, LNCS 2280, pp 342-356. 2002
PDF, Slides(PPT), MOP, DOI, TACAS'02, BIB
2001 |
---|
- Interpreting Abstract Interpretations in Membership Equational Logic
Bernd Fischer and Grigore Rosu
RULE'01, Electronic Notes in Theoretical Computer Science 59(4), pp 271-285. 2001
PDF, Maude, DOI, BIB
- Certifying Domain-Specific Policies
Michael Lowry and Thomas Pressburger and Grigore Rosu
ASE'01, IEEE, pp 81-90. 2001
PDF, Slides(PPT), AutoFilter, DOI, ASE'01, BIB
- Monitoring Programs using Rewriting
Klaus Havelund and Grigore Rosu
ASE'01, IEEE, pp 135-143. 2001
PDF, Slides(PPT), MOP, DOI, ASE'01, BIB
- Synthesizing Dynamic Programming Algorithms from Linear Temporal Logic Formulae
Grigore Rosu and Klaus Havelund
Technical Report https://ti.arc.nasa.gov/m/pub-archive/archive/0220.pdf, January 2001
PDF, DOI, BIB
2000 |
---|
- Hidden Logic
Grigore Rosu
PhD Thesis, University of California at San Diego
PDF, Thesis@UCSD, BIB
- Abstract Semantics for Module Composition
Grigore Rosu
Technical Report http://roger.ucsd.edu/record=b7304233~S9, May 2000
PDF, DOI, BIB
1999 |
---|
1998 |
---|
1997 |
---|
1996 |
---|