FSL Publications
From FSL
Here are all the papers published by the FSL group. Older publications by Grigore Rosu (before joining UIUC) can be found on his previous publications page.
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
- Converting Parallel Code from Low-Level Abstractions to Higher-Level Abstractions
Semih Okur and Cansu Erdogan and Danny Dig
ECOOP'14, Springer, pp 515-540. 2014
PDF, Taskifier, DOI, ECOOP'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
- Optimizing SYB is Easy!
Michael D. Adams and Andrew Farmer and Jose Pedro Magalhaes
PEPM'14, ACM, pp 71-82. 2014
PDF, Optimizing SYB, DOI, PEPM'14, 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
- Efficient, Expressive, and Effective Runtime Verification
Patrick Meredith
PhD Thesis, University of Illinois, August 2012
PDF, Slides(KEY), Slides(PDF), JavaMOP Project, BusMOP Project, RV-Predict Project, BIB
- Making Runtime Monitoring of Parametric Properties Practical
Dongyun Jin
PhD Thesis, University of Illinois, August 2012
PDF, Slides (PDF), JavaMOP, Sources, 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
- A Formal Semantics of C with Applications
Chucky Ellison
PhD Thesis, University of Illinois, July 2012
PDF, Slides, Project, BIB
- 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
- 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
- Test-Case Reduction for C Compiler Bugs
John Regehr, Yang Chen, Pascal Cuoq, Eric Eide, Chucky Ellison and Xuejun Yang
PLDI'12, ACM, pp 335-346. 2012
PDF, Slides(PPT), Project, ACM, PLDI'12, DBLP, 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
- Recursive Proofs for Inductive Tree Data-Structures
Parthasarathy Madhusudan, Xiaokang Qiu and Andrei Stefanescu
POPL'12, ACM, pp 123-136, 2012
PDF, Slides(pptx), Slides(pdf), Dryad, ACM, POPL'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
2012(NEW)
- On Safety Properties and Their Monitoring
Grigore Rosu
SACS, Volume 22(2), pp 327-365. 2012
PDF, MOP, DOI, SACS, 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, DOI, OOPSLA'12, BIB
- 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, Slides(PDF), K, DOI, ICGT'12, BIB
- Maximal Causal Models for Sequentially Consistent Systems
Traian Florin Serbanuta and Feng Chen and Grigore Rosu
RV'12, LNCS 7687, pp 136-150. 2012
PDF, Slides(PDF), JPredictor, DOI, RV'12, BIB
- 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, DOI, FM'12, BIB
- Executing Formal Semantics with the K Tool
David Lazar and Andrei Arusoaie and Traian Florin Serbanuta and Chucky Ellison and Radu Mereuta and Dorel Lucanu and Grigore Rosu
FM'12, LNCS 7436, pp 267-271. 2012
PDF, Slides(PDF), K, DOI, FM'12, BIB
- Making Runtime Monitoring of Parametric Properties Practical
Dongyun Jin
PhD Thesis, University of Illinois at Urbana-Champaign. August 2012
PDF, MOP, DOI, BIB
- Efficient, Expressive, and Effective Runtime Verification
Patrick O'Neil Meredith
PhD Thesis, University of Illinois at Urbana-Champaign. August 2012
PDF, MOP, DOI, BIB
- Reachability Logic
Grigore Rosu and Andrei Stefanescu and Stefan Ciobaca and Brandon Moore
Technical Report http://hdl.handle.net/2142/32952, Jul 2012
PDF, Reachability Logic, DOI, 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, DOI, ICALP'12, BIB
- A Formal Semantics of C with Applications
Chucky Ellison
PhD Thesis, University of Illinois. July 2012
PDF, K, DOI, BIB
- Test-Case Reduction for C Compiler Bugs
John Regehr and Yang Chen and Pascal Cuoq and Eric Eide and Chucky Ellison and Xuejun Yang
PLDI'12, ACM, pp 335-346. 2012
PDF, Slides(PPTX), C-Reduce, DOI, PLDI'12, BIB
- JavaMOP: Efficient Parametric Runtime Monitoring Framework
Dongyun Jin and Patrick O'Neil Meredith and Choonghwan Lee and Grigore Rosu
ICSE'12, IEEE, pp 1427-1430. 2012
PDF, MOP, DOI, ICSE'12, BIB
- Security-Policy Monitoring and Enforcement with JavaMOP
Soha Hussein and Patrick Meredith and Grigore Rosu
PLAS'12, ACM, pp 3:1-3:11. 2012
PDF, MOP, DOI, PLAS'12, BIB
- Defining the Undefinedness of C
Chucky Ellison and Grigore Rosu
Technical Report http://hdl.handle.net/2142/30780, April 2012
PDF, K, DOI, BIB
- Scalable Parametric Runtime Monitoring
Dongyun Jin and Patrick O'Neil Meredith and Grigore Rosu
Technical Report http://hdl.handle.net/2142/30757, April 2012
PDF, MOP, DOI, BIB
- Towards Categorizing and Formalizing the JDK API
Choonghwan Lee and Dongyun Jin and Patrick O'Neil Meredith and Grigore Rosu
Technical Report http://hdl.handle.net/2142/30006, March 2012
PDF, Java API, DOI, BIB
- Making Maude Definitions more Interactive
Andrei Arusoaie and Traian Florin Serbanuta and Chucky Ellison and Grigore Rosu
WRLA'12, LNCS 7571, pp 83-98. 2012
PDF, K, DOI, WRLA'12, BIB
- K Framework Distilled
Dorel Lucanu and Traian Florin Serbanuta and Grigore Rosu
WRLA'12, LNCS 7571, pp 31-53. 2012
PDF, K, DOI, WRLA'12, BIB
- Semantics and Algorithms for Parametric Monitoring
Grigore Rosu and Feng Chen
J.LMCS, Volume 8(1), pp 1-47. 2012
PDF, MOP, DOI, J.LMCS, BIB
- An Executable Formal Semantics of C with Applications
Chucky Ellison and Grigore Rosu
POPL'12, ACM, pp 533-544. 2012
PDF, Slides(PDF), Semantics, DOI, POPL'12, BIB
- Recursive Proofs for Inductive Tree Data-Structures
Parthasarathy Madhusudan and Xiaokang Qiu and Andrei Stefanescu
POPL'12, ACM, pp 123-136. 2012
PDF, Dryad, DOI, POPL'12, 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
2011(NEW)
- 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
- MatchC: A Matching Logic Reachability Verifier Using the K Framework
Andrei Stefanescu
K'11, ENTCS 304. 2011
PDF, Matching Logic, DOI, 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
- A Rewriting Approach to Concurrent Programming Language Design and Semantics
Traian Florin Serbanuta
PhD Thesis, University of Illinois, December 2010
PDF, Slides (PDF), K-Maude, TR@UIUC, 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
- Ambient intelligence in self-organising assembly systems using the chemical reaction model
Regina Frei, Giovanna Di Marzo Serugendo and Traian Florin Serbanuta
J. of Ambient Intelligence and Humanized Computing, Volume 1(3), pp 163-184. 2010
J.AIHC, 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
- Handling Mixed-Criticality in SoC-based Real-Time Embedded Systems
Rodolfo Pellizzoni, Patrick Meredith, Min-Young Nam, Mu Sun, Marco Caccamo and Lui Sha
Emsoft'09, ACM, pp 235--244. 2009
PDF, Slides(PPTX), ACM, Emsoft'09, 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 Defining Type Systems
Chucky Ellison
Master's Thesis
PDF, TR@UIUC, 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
- Memory Representations in Rewriting Logic Semantics Definitions
Mark Hills
WRLA'08, ENTCS, to appear, 2008
PDF, WRLA'08 slides, WRLA'08, 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
- 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 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
- 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
- Discovering Likely Method Specifications
Nikolai Tillmann and Feng Chen and Wolfram Schulte
ICFEM'06, to appear in LNCS, 2006
PDF, ICFEM'06, 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
- 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
- Parametric and Termination-Sensitive Control Dependence
Feng Chen and Grigore Rosu
Technical report UIUCDCS-R-2006-2712, April 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
- 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
- Predicting Concurrency Errors at Runtime using Sliced Causality
Feng Chen and Grigore Rosu
Technical report UIUCDCS-R-2005-2660, 2005.
PDF, TR@UIUC, 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
2005(NEW)
- 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
- 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
- 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
- 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
- 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