PyMOP: A Runtime Verification Tool for Python

Abstract

Runtime verification (RV) now scales for testing in thousands of open-source Java projects, helping find hundreds of bugs by monitoring test executions against formal specifications (specs). The popular Python ecosystem could use such benefits. But, current Python RV tools are limited to a domain or spec logic, or they are slow. We present PyMOP, a generic, extensible, and more efficient Python RV tool. PyMOP supports five logics, implements five monitoring algorithms, ships with 81 specs, and supports three instrumentation strategies. On 48,090 unit tests in 839 GitHub projects, we find mainly that (i) PyMOP is up to 419.23x faster than two recent dynamic analysis tools; (ii) Expensive instrumentation is a main cause of RV's runtime overhead for Python; and (iii) 84 of 156 bugs that PyMOP found were confirmed or fixed by developers. PyMOP's genericness and efficiency position it well as an excellent platform for the next advances on RV for Python. PyMOP is at https://github.com/SoftEngResearch/pymop and a video demo is at https://pymop.zhuohangshen.com/demo.