Runtime Verification
From FSL
Runtime verification is a computing system analysis and execution approach based on extracting information from a running system and using it to detect and possibly react to observed behaviors satisfying or violating certain properties. Some very particular properties, such as datarace and deadlock freedom, are typically desired to be satisfied by all systems and may be best implemented algorithmically. Other properties can be more conveniently captured as formal specifications. Runtime verification specifications are typically expressed in trace predicate formalisms, such as finite state machines, regular expressions, context-free patterns, linear temporal logics, etc., or extensions of these. This allows for a less adhoc approach than normal testing. However, any mechanism for monitoring an executing system is considered runtime verification, including verifying against test oracles and reference implementations. When formal requirements specifications are provided, monitors are synthesized from them and infused within the system by means of instrumentation. Runtime verification can be used for many purposes, such as security or safety policy monitoring, debugging, testing, verification, validation, profiling, fault protection, behavior modification (e.g., recovery), etc. Runtime verification avoids the complexity of traditional formal verification techniques, such as model checking and theorem proving, by analyzing only one or a few execution traces and by working directly with the actual system, thus scaling up relatively well and giving more confidence in the results of the analysis (because it avoids the tedious and error-prone step of formally modelling the system), at the expense of less coverage. Moreover, through its reflective capabilities runtime verification can be made an integral part of the target system, monitoring and guiding its execution during deployment.
The terminology runtime verification was formally introduced as the name of a 2001 workshop, organized by Klaus Havelund and Grigore Rosu, aimed at addressing problems at the boundary between formal verification and testing. For more information and examples, we refer the interested reader to the Wikipedia runtime verification page:
FSL Research on Runtime Verification
We do runtime verification research on the following specific topics:
FSL Publications on Runtime Verification
Below is the list of all our publications that are directly or indirectly related to runtime verification, in reverse chronological order. If interested in publications on specific topics then click on the links above.
- 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- 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- 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- 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- 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- 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- 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- 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- On Safety Properties and Their Monitoring
- Grigore Rosu
SACS, Volume 22(2), pp 327-365. 2012
PDF, MOP, DOI, SACS, 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- 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- 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- 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- 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- 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- 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- Runtime Verification with the RV System
- Patrick Meredith and Grigore Rosu
RV'10, Springer, pp 136-152. 2010
PDF, Slides(PPT), Slides(PDF), RV, DOI, RV'10, BIB- Maximal Causal Models for Sequentially Consistent Multithreaded Systems
- Traian Florin Serbanuta and Feng Chen and Grigore Rosu
Technical Report http://hdl.handle.net/2142/17336, September 2010
PDF, JPredictor, DOI, 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- 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- 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- 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- 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
- 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- 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- 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- 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- 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- 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- 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- 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- 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- 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- 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- 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- 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- 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- 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- 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- 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- 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- 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- On Safety Properties and Their Monitoring
- Grigore Rosu
Technical report UIUCDCS-R-2007-2850, February 2007
PDF, ZIP, TR@UIUC, 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- 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- 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- 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- Efficient Monitoring of Safety Properties
- Klaus Havelund and Grigore Rosu
J. of STTT, Volume 6(2), pp 158-173. 2004
PDF, J.STTT, 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- 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
