Runtime verification (RV) monitors program executions for conformance with formal specifications (specs). This paper concerns Monitoring-Oriented Programming (MOP), the only RV approach shown to scale to thousands of open-source GitHub projects when simultaneously monitoring passing unit tests against dozens of specs. Explicitly storing traces—sequences of spec-related program events—can make it easier to debug spec violations or to monitor tests against hyperproperties, which requires reasoning about sets of traces. But, most online MOP algorithms are implicit trace , i.e. they work event by event to avoid the time and space costs of storing traces. Yet, T race MOP, the only explicit-trace online MOP algorithm, is often too slow and often fails. We propose L azy MOP, a faster explicit-trace online MOP algorithm for RV of tests that is enabled by three simple optimizations. First, whereas all existing online MOP algorithms eagerly monitor all events as they occur, L azy MOP lazily stores only unique traces at runtime and monitors them just before the test run ends. Lazy monitoring is inspired by a recent finding: 99.87% of traces during RV of tests are duplicates. Second, to speed up trace storage, L azy MOP encodes events and their locations as integers, and amortizes the cost of looking up locations across events. Lastly, L azy MOP only synchronizes accesses to its trace store after detecting multi-threading, unlike T race MOP’s eager and wasteful synchronization of all accesses. On 179 Java open-source projects, L azy MOP is up to 4.9 x faster and uses 4.8 x less memory than T race MOP, finding the same traces (modulo test non-determinism) and violations. We show L azy MOP’s usefulness in the context of software evolution, where tests are re-run after each code change. L azy MOP e optimizes L azy MOP in this context by generating fewer duplicate traces. Using unique traces from one code version, L azy MOP e finds all pairs of method m and spec s , where all traces for s in m are identical. Then, in a future version, L azy MOP e generates and monitors only one trace of s in m . L azy MOP e is up to 3.9 x faster than L azy MOP and it speeds up two recent techniques that speed up RV during evolution by up to 4.6 x with no loss in violations.

@article{paperbot2920,
  title = {Faster Explicit-Trace Monitoring-Oriented Programming for Runtime Verification of Software Tests},
  author = {Kevin Guan and Marcelo d'Amorim and Owolabi Legunsen},
  journal = {Proceedings of the ACM on Programming Languages},
  volume = {9},
  number = {OOPSLA2},
  year = {2025},
  doi = {10.1145/3763183}
}