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.
Thu 9 JulDisplayed time zone: Eastern Time (US & Canada) change
14:00 - 15:30 | Verification 2Tool Demonstrations / Ideas, Visions and Reflections / Research Papers at MB 3.435 Chair(s): Shiva Nejati University of Ottawa | ||
14:00 20mTalk | Agentic Verification of Software Systems Research Papers Haoxin Tu National University of Singapore, Huan Zhao National University of Singapore, Yahui Song Standard Chartered Bank, Mehtab Zafar National University of Singapore, Ruijie Meng CISPA Helmholtz Center for Information Security, Abhik Roychoudhury National University of Singapore Pre-print | ||
14:20 20mTalk | DiverFPS: Generating Diverse Solutions for Floating-Point SMT Formulas Research Papers Shuangyu Lyu Beihang University, Chuan Luo Beihang University, Ruizhi Shi Beihang University, Zhuo Su Beihang University, Chunming Hu Beihang University | ||
14:40 10mTalk | The Watermark Paradox: How Provenance Verification Paves the Road to Camouflaged Backdoors Ideas, Visions and Reflections Haoyi Zhang Xi’an Jiaotong-Liverpool University, Huaijin Ran Xi’an Jiaotong-Liverpool University, Kisub Kim DGIST, Xunzhu Tang University of Luxembourg DOI | ||
14:50 10mTalk | HarnessForge: Automated Extraction of Verification Tasks from Industry-Scale Software Projects Tool Demonstrations Dirk Beyer LMU Munich, Po-Chun Chien LMU Munich, Bo-Yuan Huang Intel, USA, Nian-Ze Lee National Taiwan University, Taiwan, Thomas Lemberger LMU Munich Pre-print Media Attached | ||
15:00 10mTalk | PyMOP: A Runtime Verification Tool for Python Tool Demonstrations Zhuohang Shen Cornell University, Mohammed S. Yaseen Independent Researcher, Kevin Guan Cornell University, Denini Silva Federal University of Pernambuco, Marcelo d'Amorim North Carolina State University, Owolabi Legunsen Cornell University | ||
15:10 20mTalk | Property Refinement in Linear Temporal Logic: Formal Semantics and Algorithms for Software Verification Research Papers Luca Brodo Hochschule Hamm-Lippstadt, Giuseppe Scalora Hamm-Lippstadt University of Applied Sciences, Stefan Henkler Hochschule Hamm-Lippstadt File Attached | ||