一句话：提出 Lazy MOP，通过惰性存储唯一轨迹等三项优化，显著加速显式轨迹在线 MOP 的软件测试运行时验证。
运行时验证（RV）监控执行是否满足形式规约。监控导向编程（MOP）是唯一能扩展到数千 GitHub 项目、同时监控通过单元测试与数十条规约的 RV 方法。显式存储轨迹利于调试违规或监控超性质，但唯一显式轨迹在线算法 TraceMOP 过慢且常失败。本文提出 Lazy MOP，三项优化：利用 99.87% 轨迹重复，仅惰性存唯一轨迹并在测试结束前监控；将事件及位置编码为整数并摊销查找；仅在检测到多线程后同步轨迹存储。在 179 个 Java 开源项目上，其比 TraceMOP 快至 4.9 倍、内存少 4.8 倍，发现相同轨迹与违规。面向软件演化的 Lazy MOPe 进一步减少重复轨迹，比 Lazy MOP 快至 3.9 倍，并使两种演化期 RV 加速技术提速至 4.6 倍且无违规遗漏。
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}
}