Pith. sign in

REVIEW 3 major objections 4 minor 172 references

A Generic and Efficient Python Runtime Verification System and its Large-scale Evaluation

T0 review · 3 major / 4 minor · reviewed 2026-08-15 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read PyMOP is a generic and efficient runtime verification system for Python, the first monitoring-oriented programming instance for Python, and its 1,463-project evaluation shows that the JavaMOP default algorithm is often not the fastest for…

desk verdict A solid, transparently evaluated first MOP-style runtime verification system for Python; treat the headline 1,168.3x speedup as a self-reported upper bound until the private DynaPyt-with-libraries configuration is released. read the letter →

arxiv 2509.06324 v1 pith:UJ4DRR2O submitted 2025-09-08 cs.SE

Zhuohang Shen , Mohammed Yaseen , Denini Silva , Kevin Guan , Junho Lee , Marcelo d'Amorim , Owolabi Legunsen This is my paper · ORCID
classification cs.SE
keywords runtimeverificationPythonmonitoring-orientedprogrammingparametrictraceslicingdynamicanalysisAPIspecificationspytestbugfinding
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

PyMOP is a runtime verification system for Python and the first Python instance of monitoring-oriented programming. The paper's central claim is that generic RV for Python can be efficient enough to run while testing thousands of real projects: PyMOP combines five specification logics, five monitoring algorithms, three instrumentation strategies, and 73 handwritten API specs. In a large-scale evaluation on 290,133 unit tests from 1,463 GitHub projects, the authors report that the monitoring algorithm that is the default for Java is fastest for Python in only 69.3% of projects, and that PyMOP is up to 1,168.3x faster than two recent dynamic-analysis systems. They also report that 44 of 121 bugs PyMOP helped find were confirmed or fixed by developers, indicating API-level specifications can surface real defects during ordinary Python testing.

What carries the argument

The central mechanism is parametric trace slicing: a parametric trace is decomposed into per-object non-parametric slices so that an event about object f1 is not conflated with the same event about f2. On top of that decomposition, the D⟨X⟩ algorithm computes enable sets for each spec, meaning the sets of parameters that must be bound for the current slice to still reach a category of interest, so it can avoid instantiating monitors that can never matter. PyMOP implements five trace-slicing algorithms and a monitor garbage-collection pass that uses coenable sets to drop monitors that can no longer reach a verdict; this machinery is what lets many specs be checked simultaneously without the overhead of earlier Python RV systems.

What would settle it

Run the same 73 specs and 1,463 projects on a differently chosen set of open-source Python projects, such as a random sample of popular packages rather than projects that mention the six covered libraries, and check whether D⟨X⟩ is still the fastest in about 69.3% of projects and whether the speedup over DynaPyt with libraries stays above 1,000x; independently, rebuild that configuration using only the public DynaPyt API to see whether the RQ4 gap persists.

Watch

Extended reading notes

Core claim

The paper shows that a monitoring-oriented-programming style parametric runtime monitor can be built for Python without giving up on either generality or speed. Genericity is achieved by compiling specs written in past- and future-time LTL, extended regular expressions, FSMs, or context-free grammars into monitor templates, and by supporting three instrumentation strategies: monkey patching, monkey patching plus C-level patching, and monkey patching plus AST rewriting. Efficiency is achieved by implementing the parametric trace-slicing algorithms A⟨X⟩, B⟨X⟩, C⟨X⟩, C+⟨X⟩, and D⟨X⟩ as libraries, with D⟨X⟩ using spec-derived enable sets to avoid creating monitors that cannot reach a verdict. The headline finding is that D⟨X⟩, the only algorithm that the Java MOP system implements, is the fastest in 69.3% of 1,437 projects, but that the simpler algorithms are within two seconds of the fastest in 59.1% of projects and within five seconds in 68.1%. The paper also reports that PyMOP, while monitoring more code than the two comparison dynamic analyzers, is up to 419.97x faster than those tools without library monitoring and up to 1,168.3x faster than one of them with library monitoring.

Load-bearing premise

The findings assume that the 73 handwritten API specs and 1,463 GitHub projects chosen because they mention six covered libraries are representative of Python development, and that the DynaPyt-with-libraries setup built from private communication is a fair comparison; if either assumption fails, the speed rankings and speedup numbers may not generalize.

Editorial extensions

If this is right

  • D⟨X⟩ is the fastest algorithm in 69.3% of the 1,437 projects, but with a two-second tolerance the algorithm choice does not matter in 59.1% of projects, so a simpler algorithm is often a practical default.
  • Because PyMOP reimplements all five algorithms in one framework, future work can study which algorithm suits which project or spec type on the same corpus instead of comparing across different systems.
  • The 44 confirmed or fixed bugs, including TOCTOU violations in a popular MySQL client and four bugs in the Python interpreter itself, show that API-level specs can catch real defects during ordinary pytest runs.
  • Differential testing against the two dynamic analyzers found violations each tool missed alone, with 11 found only by PyMOP and 9 found only by the library-instrumented analyzer, so multiple RV systems and specs are complementary rather than interchangeable.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • If the 1,463-project corpus is representative, the 69.3% figure implies that algorithm selection for Python RV should be data-driven and workload-specific, not inherited from Java's default; a project could cheaply benchmark D⟨X⟩ against C+⟨X⟩ on its own tests.
  • The largest speedup figure depends on a DynaPyt-with-libraries configuration that was built from private communication with DynaPyt's authors; re-running the comparison with the public API or a third-party implementation would test how robust that gap is.
  • Because PyMOP currently starts monitoring only when pytest loads it, it misses events that occur before pytest starts; moving to sitecustomize.py, which the paper names as future work, could change both the violation counts and extend monitoring beyond testing.
  • The monitor garbage-collection results, with 645 projects faster and 718 slower, suggest that MGC should be enabled selectively, probably for specs with multiple parameter types, rather than always on.
Share X Bluesky LinkedIn Reddit HN

Signed reviews

No signed human review yet.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

3 major / 4 minor

Summary. The paper introduces PyMOP, a pytest-based runtime verification (RV) system for Python and the first Monitoring-Oriented Programming (MOP) instance for Python. PyMOP is claimed to be generic and extensible: it supports five specification logics, five trace-slicing monitoring algorithms, three instrumentation strategies, and ships with 73 API specifications for the Python runtime and popular libraries. The evaluation runs 290,133 unit tests across 1,463 GitHub projects and compares PyMOP's algorithms, instrumentation strategies, and bug-finding effectiveness against two existing Python dynamic analyzers, DynaPyt and DyLin. The main reported findings are that the JavaMOP default algorithm D<X> is fastest in 69.3% of projects, that PyMOP is up to 1,168.3x faster than DynaPyt and DyLin, and that 44 of 121 bugs found with PyMOP were confirmed or fixed by developers, including four in the CPython interpreter.

Significance. If the results hold, PyMOP is a substantial systems contribution: it fills a real gap in Python RV, provides a modular architecture that can host multiple logics and algorithms, and its evaluation is unusually careful for the area. I credit the paper for defining robustness as matching baseline outcomes, using non-parametric statistical tests with Bonferroni correction, reporting overhead distributions rather than only means, stating limitations explicitly, and making an artifact available. The bug-finding results, with maintainer confirmations and CPython bug reports, are also valuable evidence of practical impact. However, the paper's headline efficiency claim against DynaPyt and DyLin currently depends on a privately communicated configuration and a survivor-only subset, and one abstract claim is worded inconsistently with the paper's own data. The significance is therefore conditional on making that comparison reproducible or appropriately reframing the claim.

major comments (3)
  1. [4.5, Table 7, Figure 6] The abstract and Section 1 claim 'PyMOP is up to 1,168.3x faster than two recent dynamic analysis systems,' but this number is computed only against the DynaPyt-with-libraries configuration, which was built 'with input from their authors' via private communication [57] and is not shipped or specified in the artifact. Table 7 reports 2,000,000 seconds of instrumentation time for that configuration, and Section 4.5 states that it succeeds in only 935 of 1,463 projects; the RQ4 statistics use only the 840 projects where all four configurations succeed. The strongest quantitative claim is therefore based on an unreproducible baseline and a censored survivor subset. Please release the exact configuration and scripts, or state clearly in the abstract and in RQ4 that the 1,168.3x figure is self-reported for a non-public configuration and is computed over survivors only.
  2. [Abstract and Section 4.2] The abstract's first finding, that 'the default monitoring algorithm for Java is often not the fastest for Python,' is contradicted by the paper's own data. Section 4.2 and Figure 5 report that D<X> is the fastest algorithm in 996 of 1,437 projects, i.e., 69.3% of projects, which is a majority; the 'same within 2s/5s' analysis shows that simple algorithms are competitive only under a tolerance threshold. The claim should be reworded to say that D<X> is not always fastest, or that the choice often does not matter within a small tolerance, rather than that the Java default is 'often not' the fastest.
  3. [Abstract, Section 1, Table 6] The abstract states that '44 of 121 bugs that PyMOP helped find so far were fixed by developers,' but the text in Section 1 says '44 were confirmed or fixed,' and Table 6 reports 39+5 accepted pull requests/issues and 7+5 rejected. Confirming a bug, or having a pull request accepted, is not the same as having the bug fixed, and several reports are pending. Please reconcile the wording with the underlying counts and avoid implying that all 44 were fixed in the released code.
minor comments (4)
  1. [4.5] The relationship between the 935 projects where DynaPyt-with-libraries succeeds and the 840 projects used for RQ4 is not explained; please state explicitly why the latter set was used and whether the 840 are the intersection of all four configurations succeeding.
  2. [Table 6] The entries in Table 6 use a '35+2' notation, but the caption does not explain that the two numbers correspond to pull requests and issues, respectively; please add that explanation to the caption or note.
  3. [Figure 5] The legend in the top-left plot reads 'B C C+D' while the algorithm is C+; please correct the label and ensure the caption explains why C+ is elided in the bottom two plots.
  4. [4.1] The specification corpus is author-written and selected by the authors, and the response to this threat in the threats-to-validity paragraph relies on following prior work's methodology; please add a sentence on whether any external validator or user study was used for spec correctness beyond the two tests per spec.

Circularity Check

0 steps flagged · score 0.0 of 10

No circularity: PyMOP's claims are empirical measurements against external specs, algorithms, and tools, not derived from its own inputs.

full rationale

PyMOP's contribution is a system plus an empirical evaluation; there is no derivation chain in which an output is constructed from its input. The 73 specs are manually written from API documentation following the procedure of Lee et al. (Section 4.1), so they are external inputs, not products of the conclusions. The five monitoring algorithms are implementations of previously published algorithms, and the finding that D<X> is fastest in 69.3% of 1,437 projects is a measurement, not a quantity forced by the framework's design. RQ4's speedup figures compare PyMOP against independent tools (DynaPyt and DyLin) on translated checkers; although the DynaPyt-with-libraries configuration relies on private communication [57] and the 840-project subset is censored, this is a reproducibility and external-validity concern, not a circular reduction, because the baseline times are measured rather than derived from PyMOP's assumptions. The bug-finding claims rest on maintainer confirmations of 44 fixed bugs. Self-citations to MOP/JavaMOP background and previous RV work are used as context or as cited algorithms, but the paper's central claims do not reduce to those citations, and no fitted parameter is renamed as a prediction. Therefore no significant circularity is present.

Assumptions & free parameters 0 free parameters · 4 assumptions · 0 invented entities

The central claim relies on prior monitoring algorithms, the fidelity of Python instrumentation, the representativeness of the chosen project and spec corpus, and the developer-response signal. None of these are fitted constants or invented entities; they are domain assumptions explicit or implicit in the evaluation design.

assumptions (4)
  • domain assumption The correctness and complexity of parametric trace slicing and algorithms A<X>, B<X>, C<X>, C+<X>, and D<X> are as established in prior work by Chen, Rosu, Jin, Luo, and colleagues.
    PyMOP implements these algorithms as libraries, and the paper cites proofs from [29,33,109] instead of re-proving them. The central efficiency comparison inherits any errors in those implementations.
  • domain assumption Monkey-patching and curses-based instrumentation faithfully signals all relevant API events without inserting spurious events.
    RQ2 compares instrumentation strategies and RQ4's violations are counted from these signals; if instrumentation misses events or changes program behavior, overhead and bug counts would change.
  • domain assumption The 1,463-project corpus selected via library manifests is representative enough to support general conclusions about algorithm choice and tool speedups.
    Section 4.1 selects projects by mentions of nltk, requests, tensorflow, flask, tornado, and scipy; the authors note in Section 5 that another project set could yield different results.
  • domain assumption Developer responses (accepted, rejected, pending) are an unbiased signal of whether a PyMOP violation is a true bug.
    RQ3 uses 44 confirmed or fixed bugs as evidence of effectiveness; maintainer non-response and project abandonment may hide further true bugs or rejections.

how reviews work

0 comments
Cite this review

Pith. "Pith review of A Generic and Efficient Python Runtime Verification System and its Large-scale Evaluation." pith.science (2026). https://pith.science/paper/UJ4DRR2O

@misc{pith2026250906324,
  author       = {Pith},
  title        = {Pith review of: A Generic and Efficient Python Runtime Verification System and its Large-scale Evaluation},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/UJ4DRR2O}},
  note         = {Machine review of arXiv:2509.06324}
}
read the original abstract

Runtime verification (RV) now scales for testing thousands of open-source Java projects, helping find hundreds of bugs. The popular Python ecosystem could use such benefits. But, today's Python RV systems are limited to a domain or specification logic, or slow. We propose PyMOP, a generic, extensible, and efficient RV system for Python. PyMOP supports five logics, implements five existing monitoring algorithms, ships with 73 API specs of Python and widely-used libraries, supports three instrumentation strategies, and users can easily add more of these. On 290,133 unit tests in 1,463 GitHub projects, we find mainly that (i) the default monitoring algorithm for Java is often not the fastest for Python; (ii) PyMOP is up to 1,168.3x faster than two recent dynamic analysis systems; and (iii) 44 of 121 bugs that PyMOP helped find so far were fixed by developers. PyMOP's generality and efficiency position it well as an excellent platform for the next advances on RV for Python.

Figures

Figures reproduced from arXiv: 2509.06324 by the authors.

Figure 1
Figure 1. TOCTOU spec in PyMOP’s JSON-like frontend; user can also write in Python. [PITH_FULL_IMAGE:figures/full_fig_p003_1.png] view at source ↗
Figure 2
Figure 2. TOCTOU’s FSM. “Time-Of-Check to Time-Of-Use” (TOCTOU) vulner￾abilities [115] involve the trace <check permission for file f>⇝<use f>. Attackers can exploit the inter￾val between these two events, e.g., to replace f with a symbolic link or changing its contents or permis￾sions [19,165]. TOCTOU is described in Python’s doc￾umentation for os.access [126]: “Using access() to check if a user is authorized to e.g. open a … view at source ↗
Figure 3
Figure 3. Code that violates TOCTOU in MyCLI [117] TOCTOU violations found by PyMOP. We reported four TOCTOU violations that PyMOP helped us find; two were accepted or fixed, one was rejected, and the other is pending. One viola￾tion was in mycli [117], a popular command-line MySQL interface with 664 forks and 11.6K stars. The violation occurred in a function that reads passwords from a file [PITH_FULL_IMAGE:figures/full_fig… view at source ↗
Figures from the paper (4 more)
Figure 4
Figure 4. Figure 4: PyMOP’s Architecture. architecture has three main com￾ponents. Monitor Synthesizer ( 1 ) uses logic plugins to compile specs (diamonds) into code (circles) from which the Monitoring Engine ( 3 ) instantiates monitors (filled circles) at runtime. Instrumenter ( 2 ) rewr…
Figure 5
Figure 5. Figure 5: PyMOP ’s overhead in 1,437 projects, grouped by decile. First row, from left [PITH_FULL_IMAGE:figures/full_fig_p010_5.png]
Figure 6
Figure 6. Figure 6: Log scale (base 10) plot of distributions of time overhead per decile for 840 [PITH_FULL_IMAGE:figures/full_fig_p014_6.png]
Figure 7
Figure 7. Figure 7: Sets of PyMOP, DynaPyt, and DyLin violations in RQ4, explained in text. [PITH_FULL_IMAGE:figures/full_fig_p015_7.png]

Review history (2 revisions) →

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

172 extracted references · 79 canonical work pages

  1. [57]

    E-mail, e-mail reply to the authors about instrumenting third-party libraries using DynaPyt, June 2025

    Eghbali, A.: Private communication. E-mail, e-mail reply to the authors about instrumenting third-party libraries using DynaPyt, June 2025

    2025

  2. [1]

    PACMPL 3(POPL) (2019)

    Aceto, L., Achilleos, A., Francalanza, A., Ingólfsdóttir, A., Lehtinen, K.: Adven- tures in monitorability: From branching to linear time and back again. PACMPL 3(POPL) (2019)

    2019

  3. [2]

    In: SEFM (2019)

    Aceto, L., Achilleos, A., Francalanza, A., Ingólfsdóttir, A., Lehtinen, K.: An op- erational guide to monitorability. In: SEFM (2019)

    2019

  4. [3]

    In: OOPSLA (2005)

    Allan, C., Avgustinov, P., Christensen, A.S., Hendren, L., Kuzins, S., Lhoták, O., de Moor, O., Sereni, D., Sittampalam, G., Tibble, J.: Adding trace matching with free variables to AspectJ. In: OOPSLA (2005)

    2005

  5. [4]

    JSS167(2020)

    An,D.,Liu,J.,Zhang,M.,Chen,X.,Chen,M.,Sun,H.:Uncertaintymodelingand runtime verification for autonomous vehicles driving control: A machine learning- based approach. JSS167(2020)

    2020

  6. [5]

    In: OOPSLA (2008)

    Arnold, M., Vechev, M., Yahav, E.: QVM: An efficient runtime for detecting defects in deployed systems. In: OOPSLA (2008)

    2008

  7. [6]

    io/prj/artcat

    ARTCAT: Autonomic Response To Cyber-Attack, https://grammatech.github. io/prj/artcat

  8. [7]

    In: OOP- SLA (2007)

    Avgustinov, P., Tibble, J., de Moor, O.: Making trace monitors feasible. In: OOP- SLA (2007)

    2007

Show all 172 references
  1. [8]

    In: VMCAI (2004)

    Barringer, H., Goldberg, A., Havelund, K., Sen, K.: Rule-based runtime verifica- tion. In: VMCAI (2004)

    2004

  2. [9]

    Journal of Aerospace Computing, Information, and Communication7(11) (2010)

    Barringer, H., Groce, A., Havelund, K., Smith, M.: Formal analysis of log files. Journal of Aerospace Computing, Information, and Communication7(11) (2010)

    2010

  3. [10]

    Journal of Logic and Computation20(3) (2010)

    Barringer, H., Rydeheard, D., Havelund, K.: Rule systems for run-time monitor- ing: From Eagle to RuleR. Journal of Logic and Computation20(3) (2010)

    2010

  4. [11]

    IJSTTT21(1) (2019)

    Bartocci, E., Falcone, Y., Bonakdarpour, B., Colombo, C., Decker, N., Havelund, K., Joshi, Y., Klaedtke, F., Milewicz, R., Reger, G., Roşu, G., Signoles, J., Thoma, D., Zalinescu, E., Zhang, Y.: First international competition on runtime verifica- tion: Rules, benchmarks, tool...

    2019

  5. [12]

    In: Lectures on Runtime Verification (2018)

    Bartocci, E., Falcone, Y., Francalanza, A., Reger, G.: Introduction to runtime verification. In: Lectures on Runtime Verification (2018)

    2018

  6. [13]

    In: TACAS (2019)

    Bartocci, E., Falcone, Y., Reger, G.: International competition on runtime verifi- cation. In: TACAS (2019)

    2019

  7. [14]

    In: FSTTCS (2015)

    Basin, D., Klaedtke, F., Zălinescu, E.: Failure-aware runtime verification of dis- tributed systems. In: FSTTCS (2015)

    2015

  8. [15]

    In: CAV (2017)

    Basin, D., Klaedtke, F., Zălinescu, E.: Runtime verification of temporal properties over out-of-order data streams. In: CAV (2017)

    2017

  9. [16]

    TECS18(5s) (2019)

    Bataineh, O., Rosenblum, D.S., Reynolds, M.: Efficient decentralized LTL moni- toring framework using tableau technique. TECS18(5s) (2019)

    2019

  10. [17]

    arXiv preprint arXiv:1006.3638 (2010)

    Bauer, A.: Monitorability of omega-regular languages. arXiv preprint arXiv:1006.3638 (2010)

    2010 arXiv

  11. [18]

    In: FM (2012)

    Bauer, A., Falcone, Y.: Decentralised LTL monitoring. In: FM (2012)

    2012

  12. [19]

    Computer Security: Art and Science (2003)

    Bishop, M.: Program security. Computer Security: Art and Science (2003)

    2003

  13. [20]

    In: OOPSLA (2006)

    Blackburn, S.M., Garner, R., Hoffmann, C., Khang, A.M., McKinley, K.S., Bentzur, R., Diwan, A., Feinberg, D., Frampton, D., Guyer, S.Z., Hirzel, M., Hosking, A., Jump, M., Lee, H., Moss, J.E.B., Phansalkar, A., Stefanović, D., VanDrunen, T., von Dincklage, D., Wiedermann, B.: ...

    2006

  14. [21]

    In: RV Demo (2011) 17

    Bodden, E.: MOPBox: A library approach to runtime verification. In: RV Demo (2011) 17

    2011

  15. [22]

    In: ECOOP (2007)

    Bodden, E., Hendren, L., Lhoták, O.: A staged static program analysis to improve the performance of runtime monitoring. In: ECOOP (2007)

    2007

  16. [23]

    In: FSE (2008)

    Bodden, E., Lam, P., Hendren, L.: Finding programming errors earlier by evalu- ating runtime monitors ahead-of-time. In: FSE (2008)

    2008

  17. [24]

    In: FMSD

    Bonakdarpour, B., Navabpour, S., Fischmeister, S.: Time-triggered runtime ver- ification. In: FMSD. vol. 43, pp. 29–60 (2013)

    2013

  18. [25]

    In: ICCPS (2025)

    Brown, R., Nguyen, L.V., Xiang, W., Wolf, M., Tran, H.D.: Perception-based quantitative runtime verification for learning-enabled cyber-physical systems. In: ICCPS (2025)

    2025

  19. [26]

    In: LICS (2001)

    Bruns, G., Godefroid, P.: Temporal logic query checking. In: LICS (2001)

    2001

  20. [27]

    In: ICFEM

    Chen, F., d’Amorim, M., Rosu, G.: A formal monitoring-based framework for software development and analysis. In: ICFEM. pp. 357–372 (2004)

    2004

  21. [28]

    Chen, F., d’Amorim, M., Rosu, G.: Checking and correcting behaviors of Java programs at runtime with Java-MOP. In: RV. pp. 3–20 (2006)

    2006

  22. [29]

    In: ASE (2009)

    Chen, F., Meredith, P.O., Jin, D., Roşu, G.: Efficient formalism-independent mon- itoring of parametric properties. In: ASE (2009)

    2009

  23. [30]

    In: OOPSLA (2007)

    Chen,F.,Roşu,G.:MOP:Anefficientandgenericruntimeverificationframework. In: OOPSLA (2007)

    2007

  24. [31]

    In: RV (2003)

    Chen, F., Roşu, G.: Towards monitoring-oriented programming: A paradigm com- bining specification and implementation. In: RV (2003)

    2003

  25. [32]

    Chen, F., Roşu, G.: Parametric trace slicing and monitoring. Tech. Rep. UIUCDCS-R-2008-2977, Computer Science Dept., UIUC (2008)

    2008

  26. [33]

    In: TACAS (2009)

    Chen, F., Roşu, G.: Parametric trace slicing and monitoring. In: TACAS (2009)

    2009

  27. [34]

    In: RV (2023)

    Cheng, C.H., Luttenberger, M., Yan, R.: Runtime monitoring DNN-based per- ception: (via the lens of formal methods). In: RV (2023)

    2023

  28. [35]

    https://github.com/ clarete/forbiddenfruit

    Clarete, L.: Forbidden Fruit: Patch built-in Python objects. https://github.com/ clarete/forbiddenfruit

  29. [36]

    Colombo, C., Pace, G.J., Abela, P.: Offline runtime verification with real-time properties: A case study. Tech. rep. (2009)

    2009

  30. [37]

    Wiley (1971), https://books

    Conover, W.: Practical Nonparametric Statistics. Wiley (1971), https://books. google.com/books?id=NV4YAAAAIAAJ

    1971

  31. [38]

    CPython, https://github.com/python/cpython/

  32. [39]

    CPython, https://github.com/python/cpython/issues/125397

  33. [40]

    CPython, https://github.com/python/cpython/issues/130850

  34. [41]

    CPython, https://github.com/python/cpython/issues/130902

  35. [42]

    CPython, https://github.com/python/cpython/issues/132372

  36. [43]

    In: WODA (2005)

    d’Amorim, M., Havelund, K.: Event-based runtime verification of Java programs. In: WODA (2005)

    2005

  37. [44]

    In: RV (2022)

    Dams, D., Havelund, K., Kauffman, S.: A Python library for trace analysis. In: RV (2022)

    2022

  38. [45]

    In: Temporal Representation and Reasoning (2005)

    d’Angelo, B., Sankaranarayanan, S., Sánchez, C., Robinson, W., Finkbeiner, B., Sipma,H.B.,Mehrotra,S.,Manna,Z.:LOLA:Runtimemonitoringofsynchronous systems. In: Temporal Representation and Reasoning (2005)

    2005

  39. [46]

    In: RV (2019)

    Danielsson, L.M., Sánchez, C.: Decentralized stream runtime verification. In: RV (2019)

    2019

  40. [47]

    In: SAC (2019)

    Dawes, J.H., Reger, G.: Specification of temporal properties of functions for run- time verification. In: SAC (2019)

    2019

  41. [48]

    In: TACAS (2019)

    Dawes, J.H., Reger, G., Franzoni, G., Pfeiffer, A., Govi, G.: VYPR2: A framework for runtime verification of Python web services. In: TACAS (2019)

    2019

  42. [49]

    In: TACAS (2016) 18

    Decker, N., Harder, J., Scheffel, T., Schmitz, M., Thoma, D.: Runtime monitoring with union-find structures. In: TACAS (2016) 18

    2016

  43. [50]

    In: FM (2013)

    Decker, N., Leucker, M., Thoma, D.: jUnit RV–adding runtime verification to jUnit. In: FM (2013)

    2013

  44. [51]

    In: RV (2017)

    Desai, A., Dreossi, T., Seshia, S.A.: Combining model checking and runtime ver- ification for safe robotics. In: RV (2017)

    2017

  45. [52]

    TCS537(2014)

    Diekert, V., Leucker, M.: Topology, monitorable properties and runtime verifica- tion. TCS537(2014)

    2014

  46. [53]

    Journal of Robotics Applications and Technologies3(1) (2015)

    Dong, Z., Fu, Y., Fu, Y.: Runtime verification on robotics systems. Journal of Robotics Applications and Technologies3(1) (2015)

    2015

  47. [54]

    Dwyer, M.B., Purandare, R., Person, S.: Runtime verification in context: Can optimizing error detection improve fault diagnosis? In: RV (2010)

    2010

  48. [55]

    DyLin, https://github.com/sola-st/DyLin/issues/3

  49. [56]

    DyLin, https://github.com/sola-st/DyLin/pull/2/

  50. [58]

    In: FSE (2025)

    Eghbali, A., Burk, F., Pradel, M.: Dylin: A dynamic linter for Python. In: FSE (2025)

    2025

  51. [59]

    In: FSE (2022)

    Eghbali, A., Pradel, M.: Dynapyt: A dynamic analysis framework for Python. In: FSE (2022)

    2022

  52. [60]

    eMOP, https://github.com/SoftEngResearch/emop

  53. [61]

    In: IEEE S&P (2000)

    Erlingsson, U., Schneider, F.B.: IRM enforcement of Java stack inspection. In: IEEE S&P (2000)

    2000

  54. [62]

    Falcone, Y., Fernandez, J.C., Mounier, L.: What can you verify and enforce at runtime? IJSTTT14(2012)

    2012

  55. [63]

    In: En- gineering Dependable Software Systems (2013)

    Falcone, Y., Havelund, K., Reger, G.: A tutorial on runtime verification. In: En- gineering Dependable Software Systems (2013)

    2013

  56. [64]

    In: RV (2018)

    Falcone, Y., Krstić, S., Reger, G., Traytel, D.: A taxonomy for classifying runtime verification tools. In: RV (2018)

    2018

  57. [65]

    In: RV (2015)

    Falcone,Y., Ničković, D.,Reger, G., Thoma,D.: Second international competition on runtime verification. In: RV (2015)

    2015

  58. [66]

    Flask, https://github.com/pallets/flask

  59. [67]

    In: RV (2012)

    Forejt, V., Kwiatkowska, M., Parker, D., Qu, H., Ujma, M.: Incremental runtime verification of probabilistic systems. In: RV (2012)

    2012

  60. [68]

    In: RV (2017)

    Francalanza, A., Aceto, L., Achilleos, A., Attard, D.P., Cassar, I., Della Monica, D., Ingólfsdóttir, A.: A foundation for runtime monitoring. In: RV (2017)

    2017

  61. [69]

    Lectures on Runtime Verification (2018)

    Francalanza, A., Pérez, J.A., Sánchez, C.: Runtime verification for decentralised and distributed systems. Lectures on Runtime Verification (2018)

    2018

  62. [70]

    In: OPODIS (2021)

    Ganguly, R., Momtaz, A., Bonakdarpour, B.: Distributed runtime verification under partial synchrony. In: OPODIS (2021)

    2021

  63. [71]

    In: ICDCS (2022)

    Ganguly, R., Xue, Y., Jonckheere, A., Ljung, P., Schornstein, B., Bonakdarpour, B., Herlihy, M.: Distributed runtime verification of metric temporal properties for cross-chain protocols. In: ICDCS (2022)

    2022

  64. [72]

    Journal of Parallel and Distributed Computing185(2024)

    Ganguly, R., Xue, Y., Jonckheere, A., Ljung, P., Schornstein, B., Bonakdarpour, B., Herlihy, M.: Distributed runtime verification of metric temporal properties. Journal of Parallel and Distributed Computing185(2024)

    2024

  65. [73]

    In: RV (2018)

    Gorostiaga, F., Sánchez, C.: Striver: Stream runtime verification for real-time event-streams. In: RV (2018)

    2018

  66. [74]

    In: 2020 23rd Euromicro Conference on Digital System Design (DSD) (2020)

    Grieser, J., Zhang, M., Warnecke, T., Rausch, A.: Assuring the safety of end- to-end learning-based autonomous driving through runtime monitoring. In: 2020 23rd Euromicro Conference on Digital System Design (DSD) (2020)

    2020

  67. [75]

    In: ISSTA (2024) 19

    Guan, K., Legunsen, O.: An in-depth study of runtime verification overheads during software testing. In: ISSTA (2024) 19

    2024

  68. [76]

    In: ICSE (2025)

    Guan, K., Legunsen, O.: Instrumentation-driven evolution-aware runtime verifi- cation. In: ICSE (2025)

    2025

  69. [77]

    In: FSE Demo (2025)

    Guan, K., Legunsen, O.: TraceMOP: An explicit-trace runtime verification tool for Java. In: FSE Demo (2025)

    2025

  70. [78]

    In: RV (2023)

    Havelund, K., Peled, D.: Monitorability for runtime verification. In: RV (2023)

    2023

  71. [79]

    In: FMCAD (2017)

    Havelund, K., Peled, D., Ulus, D.: First order temporal logic monitoring with BDDs. In: FMCAD (2017)

    2017

  72. [80]

    In: RV (2001)

    Havelund, K., Roşu, G.: Monitoring Java programs with Java PathExplorer. In: RV (2001)

    2001

  73. [81]

    In: ASE (2001)

    Havelund, K., Roşu, G.: Monitoring programs using rewriting. In: ASE (2001)

    2001

  74. [82]

    In: TACAS (2002)

    Havelund, K., Roşu, G.: Synthesizing monitors for safety properties. In: TACAS (2002)

    2002

  75. [83]

    In: RV (2020)

    Henzinger, T.A., Saraç, N.E.: Monitorability under assumptions. In: RV (2020)

    2020

  76. [84]

    HOWARD-6042(2014)

    Hinrichs, T.L., Sistla, A.P., Zuck, L.D.: Model check what you can, runtime verify the rest. HOWARD-6042(2014)

    2014

  77. [85]

    In: RV (2014)

    Ho, H.M., Ouaknine, J., Worrell, J.: Online monitoring of metric temporal logic. In: RV (2014)

    2014

  78. [86]

    John Wiley & Sons (2013)

    Hollander, M., Wolfe, D.A., Chicken, E.: Nonparametric statistical methods. John Wiley & Sons (2013)

    2013

  79. [87]

    IJSTTT24(3) (2022)

    Huang, S., Cleaveland, R.: Temporal-logic query checking over finite data streams. IJSTTT24(3) (2022)

    2022

  80. [88]

    In: A Beginners Guide to Python 3 Programming

    Hunt, J.: Monkey patching. In: A Beginners Guide to Python 3 Programming. Springer (2023)

    2023

  81. [89]

    In: PLAS (2012)

    Hussein, S., Meredith, P., Roşu, G.: Security-policy monitoring and enforcement with JavaMOP. In: PLAS (2012)

    2012

  82. [90]

    JavaMOP, https://github.com/runtimeverification/javamop

  83. [91]

    In: APSEC (2018)

    Javed, O., Binder, W.: Large-scale evaluation of the efficiency of runtime- verification tools in the wild. In: APSEC (2018)

    2018

  84. [92]

    In: ASE Demo (2020)

    Javed, O., Dawes, J.H., Han, M., Franzoni, G., Pfeiffer, A., Reger, G., Binder, W.: PerfCI: A toolchain for automated performance testing during continuous integration of Python projects. In: ASE Demo (2020)

    2020

  85. [93]

    In: PLDI (2011)

    Jin, D., Meredith, P.O., Griffith, D., Roşu, G.: Garbage collection for monitoring parametric properties. In: PLDI (2011)

    2011

  86. [94]

    In: ICSE Demo (2012)

    Jin,D.,Meredith,P.O.,Lee,C.,Roşu,G.:JavaMOP:Efficientparametricruntime monitoring framework. In: ICSE Demo (2012)

    2012

  87. [95]

    Jin, D., Meredith, P.O., Roşu, G.: Scalable parametric runtime monitoring. Tech. rep., Computer Science Dept., UIUC (2012)

    2012

  88. [96]

    In: RV (2004)

    Karaorman, M., Freeman, J.: jMonitor: Java runtime event specification and mon- itoring library. In: RV (2004)

    2004

  89. [97]

    Comprehensive Psychology3, 11–IT (2014)

    Kerby, D.S.: The simple difference formula: An approach to teaching nonpara- metric correlation. Comprehensive Psychology3, 11–IT (2014)

    2014

  90. [98]

    In: ECOOP (2001)

    Kiczales, G., Hilsdale, E., Hugunin, J., Kersten, M., Palm, J., Griswold, W.G.: An overview of AspectJ. In: ECOOP (2001)

    2001

  91. [99]

    In: ECRTS (1999)

    Kim, M., Viswanathan, M., Ben-Abdallah, H., Kannan, S., Lee, I., Sokolsky, O.: Formally specified monitoring of temporal properties. In: ECRTS (1999)

    1999

  92. [100]

    Lee, C., Jin, D., Meredith, P.O., Roşu, G.: Towards categorizing and formalizing the JDK API. Tech. rep., Computer Science Dept., UIUC (2012)

    2012

  93. [101]

    In: ICSE NIER (2015)

    Legunsen, O., Marinov, D., Roşu, G.: Evolution-aware monitoring-oriented pro- gramming. In: ICSE NIER (2015)

    2015

  94. [102]

    In: ICST (2019) 20

    Legunsen, O., Zhang, Y., Hadzi-Tanovic, M., Roşu, G., Marinov, D.: Techniques for evolution-aware runtime verification. In: ICST (2019) 20

    2019

  95. [103]

    Legunsen, O., Awar, N.A., Xu, X., Hassan, W.U., Roşu, G., Marinov, D.: How effective are existing Java API specifications for finding bugs during runtime ver- ification? ASE Journal26(4) (2019)

    2019

  96. [104]

    In: ASE (2016)

    Legunsen, O., Hassan, W.U., Xu, X., Roşu, G., Marinov, D.: How good are the specs? A study of the bug-finding effectiveness of existing Java API specifications. In: ASE (2016)

    2016

  97. [105]

    In: Workshop on Formal Languages and Analysis of Contract-Oriented Software (2007)

    Leucker, M., Schallhart, C.: A brief account of runtime verification. In: Workshop on Formal Languages and Analysis of Contract-Oriented Software (2007)

    2007

  98. [106]

    Big Data and Cognitive Computing8(5) (2024)

    Liu, Y., Li, J.: Runtime verification-based safe marl for optimized safety pol- icy generation for multi-robot systems. Big Data and Cognitive Computing8(5) (2024)

    2024

  99. [107]

    LiveDiffer, https://github.com/manthanmtg/live_differ/pull/3/

  100. [108]

    In: COMPSAC

    Luo, C., Wang, R., Jiang, Y., Yang, K., Guan, Y., Li, X., Shi, Z.: Runtime veri- fication of robots collision avoidance case study. In: COMPSAC. vol. 1 (2018)

    2018

  101. [109]

    In: RV (2014)

    Luo, Q., Zhang, Y., Lee, C., Jin, D., Meredith, P.O., Şerbănuţă, T.F., Roşu, G.: RV-Monitor: Efficient parametric runtime verification with simultaneous proper- ties. In: RV (2014)

    2014

  102. [110]

    In: AOSD (2012)

    Marek, L., Villazón, A., Zheng, Y., Ansaloni, D., Binder, W., Qi, Z.: DiSL: A domain-specific language for bytecode instrumentation. In: AOSD (2012)

    2012

  103. [111]

    In: OOPSLA (2005)

    Martin, M., Livshits, B., Lam, M.S.: Finding application errors and security flaws using PQL: A program query language. In: OOPSLA (2005)

    2005

  104. [112]

    In: ASE (2013)

    Meredith, P., Roşu, G.: Efficient parametric runtime verification with determin- istic string rewriting. In: ASE (2013)

    2013

  105. [113]

    In: ASE (2008)

    Meredith, P., Jin, D., Chen, F., Roşu, G.: Efficient monitoring of parametric context-free patterns. In: ASE (2008)

    2008

  106. [114]

    In: ICST (2020)

    Miranda, B., Lima, I., Legunsen, O., d’Amorim, M.: Prioritizing runtime verifi- cation violations. In: ICST (2020)

    2020

  107. [115]

    https://cwe.mitre.org/data/definitions/367.html (2024)

    MITRE: CWE-367: Time-of-check Time-of-use (TOCTOU) Race Condition. https://cwe.mitre.org/data/definitions/367.html (2024)

    2024

  108. [116]

    https://github.com/ ericbodden/mopbox

    MOPBox is Monitor-Oriented Programming in a box. https://github.com/ ericbodden/mopbox

  109. [117]

    MyCLI, https://github.com/dbcli/mycli/

  110. [118]

    MyCLI, https://github.com/dbcli/mycli/pull/1203/

  111. [119]

    NLTK, https://github.com/nltk/nltk

  112. [120]

    NLTK, https://www.nltk.org/api/nltk.probability.html

  113. [121]

    In: DISC (2007)

    Ogale, V.A., Garg, V.K.: Detecting temporal logic predicates on distributed com- putations. In: DISC (2007)

    2007

  114. [122]

    https://research.redhat.com/blog/article/ efficient-runtime-verification-for-the-linux-kernel

    de Oliveira, D.B.: Efficient runtime verification for the Linux kernel. https://research.redhat.com/blog/article/ efficient-runtime-verification-for-the-linux-kernel

  115. [123]

    In: OOPSLA (2010)

    Purandare, R., Dwyer, M.B., Elbaum, S.: Monitor optimization via stutter- equivalent loop transformation. In: OOPSLA (2010)

    2010

  116. [124]

    In: ISSTA (2013)

    Purandare, R., Dwyer, M.B., Elbaum, S.: Optimizing monitoring of finite state properties through monitor compaction. In: ISSTA (2013)

    2013

  117. [125]

    Pytest, https://docs.pytest.org/en/7.2.x

  118. [126]

    Python, https://docs.python.org/3.10/library/os.html#os.access

  119. [127]

    Python, https://docs.python.org/3/library/ast.html

  120. [128]

    Python, https://docs.python.org/3/library/bisect.html

  121. [129]

    Python, https://docs.python.org/3/library/stdtypes.html#dict

  122. [130]

    Python, https://docs.python.org/3/tutorial/inputoutput.html# reading-and-writing-files 21

  123. [131]

    Python, https://wiki.python.org/moin/TimeComplexity

  124. [132]

    Python, https://docs.python.org/3/library/site.html

  125. [133]

    IEEE Access9(2021)

    Rahman, Q.M., Corke, P., Dayoub, F.: Run-time monitoring of machine learning for robotic perception: A survey of emerging trends. IEEE Access9(2021)

    2021

  126. [134]

    In: TACAS (2015)

    Reger, G., Cruz, H.C., Rydeheard, D.: MarQ: Monitoring at runtime with QEA. In: TACAS (2015)

    2015

  127. [135]

    In: RV (2016)

    Reger, G., Hallé, S., Falcone, Y.: Third international competition on runtime verification. In: RV (2016)

    2016

  128. [136]

    In: International Symposium on Leveraging Applications of Formal Methods

    Reger, G., Havelund, K.: What is a trace? A runtime verification perspective. In: International Symposium on Leveraging Applications of Formal Methods. pp. 339–355 (2016)

    2016

  129. [137]

    Master’s thesis, KTH, Sweden (2014)

    Renberg, A.: Test-inspired runtime verification: Using a unit test-like specification syntax for runtime verification. Master’s thesis, KTH, Sweden (2014)

    2014

  130. [138]

    Requests, https://github.com/psf/requests

  131. [139]

    Requests, https://requests.readthedocs.io/en/latest/api/

  132. [140]

    Scientific Annals of Com- puter Science22(2) (2012)

    Rosu, G.: On safety properties and their monitoring. Scientific Annals of Com- puter Science22(2) (2012)

    2012

  133. [141]

    In: CAV (2006)

    Roşu, G., Bensalem, S.: Allen linear (interval) temporal logic – Translation to LTL and monitor synthesis. In: CAV (2006)

    2006

  134. [142]

    LICS 8(2012)

    Rosu, G., Chen, F.: Semantics and algorithms for parametric monitoring. LICS 8(2012)

    2012

  135. [143]

    https://github.com/runtimeverification/ rv-monitor

    RV-Monitor core system code. https://github.com/runtimeverification/ rv-monitor

  136. [144]

    FMSD54(2019)

    Sánchez, C., Schneider, G., Ahrendt, W., Bartocci, E., Bianculli, D., Colombo, C., Falcone, Y., Francalanza, A., Krstić, S., Lourenço, J.M., et al.: A survey of challenges for runtime verification from advanced application domains (beyond software). FMSD54(2019)

    2019

  137. [145]

    TISSEC3(1) (2000)

    Schneider, F.B.: Enforceable Security Policies. TISSEC3(1) (2000)

    2000

  138. [146]

    In: RV (2019)

    Schneider, J., Basin, D., Krstić, S., Traytel, D.: A formally verified monitor for metric first-order temporal logic. In: RV (2019)

    2019

  139. [147]

    SciPy, https://github.com/scipy/scipy

  140. [148]

    In: Advances in Computing Science – ASIAN (2003)

    Sen, K., Roşu, G., Agha, G.: Generating Optimal Linear Temporal Logic Monitors by Coinduction. In: Advances in Computing Science – ASIAN (2003)

    2003

  141. [149]

    In: ICSE (2004)

    Sen, K., Vardhan, A., Agha, G., Rosu, G.: Efficient decentralized monitoring of safety in distributed systems. In: ICSE (2004)

    2004

  142. [150]

    In: Network Meets AI & ML (2019)

    Shukla, A., Hudemann, K.N., Hecker, A., Schmid, S.: Runtime verification of p4 switches with reinforcement learning. In: Network Meets AI & ML (2019)

    2019

  143. [151]

    In: RV (2023)

    Soueidi, C., Falcone, Y.: Bridging the gap: A focused DSL for RV-oriented instru- mentation with BISM. In: RV (2023)

    2023

  144. [152]

    In: RV (2023)

    Soueidi, C., Falcone, Y.: Instrumentation for RV: From basic monitoring to ad- vanced use cases. In: RV (2023)

    2023

  145. [153]

    In: ISSRE (2023)

    Soueidi, C., Falcone, Y., Hallé, S.: Dynamic program analysis with flexible instru- mentation and complex event processing. In: ISSRE (2023)

    2023

  146. [154]

    IJSTTT25(4) (2023)

    Soueidi, C., Monnier, M., Falcone, Y.: Efficient and expressive bytecode-level instrumentation for Java programs. IJSTTT25(4) (2023)

    2023

  147. [155]

    Computer Science Review50(2023)

    Taleb, R., Hallé, S., Khoury, R.: Uncertainty in runtime verification: A survey. Computer Science Review50(2023)

    2023

  148. [156]

    In: ICST

    Teixeira, L., Miranda, B., Rebêlo, H., d’Amorim, M.: Demystifying the challenges of formally specifying api properties for runtime verification. In: ICST. pp. 82–93 (2021) 22

    2021

  149. [157]

    TensorFlow, https://github.com/tensorflow/tensorflow

  150. [158]

    In: RV (2004)

    Thati, P., Rosu, G.: Monitoring algorithms for metric temporal logic specifica- tions. In: RV (2004)

    2004

  151. [159]

    TIOBE Index, https://www.tiobe.com/tiobe-index

  152. [160]

    Tornado Web Server, https://github.com/tornadoweb/tornado

  153. [161]

    web.RequestHandler.render

    Tornado web server, https://www.tornadoweb.org/en/stable/web.html#tornado. web.RequestHandler.render

  154. [162]

    IEEE Access (2025)

    Torpmann-Hagen, B., Riegler, M.A., Halvorsen, P., Johansen, D.: Runtime veri- fication for visual deep learning systems with loss prediction. IEEE Access (2025)

    2025

  155. [163]

    TSE (2023)

    Torres, A., Costa, P., Amaral, L., Pastro, J., Bonifácio, R., d’Amorim, M., Le- gunsen, O., Bodden, E., Canedo, E.D.: Runtime verification of crypto APIs: An empirical study. TSE (2023)

    2023

  156. [164]

    (2024), https: //github.com/SoftEngResearch/tracemop

    TraceMOP: A Trace-Aware Runtime Verification Tool for Java. (2024), https: //github.com/SoftEngResearch/tracemop

    2024

  157. [165]

    In: FAST

    Wei, J., Pu, C.: Tocttou vulnerabilities in unix-style file systems: An anatomical study. In: FAST. vol. 5, pp. 12–12 (2005)

    2005

  158. [166]

    In: RV (2013)

    Wu, C.W.W., Kumar, D., Bonakdarpour, B., Fischmeister, S.: Reducing monitor- ing overhead by integrating event- and time-triggered techniques. In: RV (2013)

    2013

  159. [167]

    In: RV (2024)

    Yang, F., Zhan, S.S., Wang, Y., Huang, C., Zhu, Q.: Case study: Runtime safety verification of neural network controlled system. In: RV (2024)

    2024

  160. [168]

    In: OSDI (2020)

    Yaseen, N., Arzani, B., Beckett, R., Ciraci, S., Liu, V.: Aragog: Scalable runtime verification of shardable networked systems. In: OSDI (2020)

    2020

  161. [169]

    In: RV (2023)

    Yorihiro, A., Jiang, P., Marques, V., Carleton, B., Legunsen, O.: eMOP: A Maven plugin for evolution-aware runtime verification. In: RV (2023)

    2023

  162. [170]

    In: RV (2020)

    Zapridou, E., Bartocci, E., Katsaros, P.: Runtime verification of autonomous driv- ing systems in CARLA. In: RV (2020)

    2020

  163. [171]

    arXiv preprint arXiv:2505.18585 (2025)

    Zhang, Y., Emma, S.Y., En, A.L.J., Dong, J.S.: RvLLM: LLM Runtime Verifica- tion with Domain Knowledge. arXiv preprint arXiv:2505.18585 (2025)

    2025

  164. [172]

    In: ISSREW

    Zhou, W., Hu, F., Ma, J.: Improving Flexibility in Embedded System Runtime Verification with Python. In: ISSREW. pp. 281–282 (2022) 23

    2022

Pith tools

Reviewed August 15, 2026 · model on record in the stance chip above.