We present TraceMOP, an explicit-trace runtime verification (RV) tool. RV monitors if execution traces – sequences of events, e.g., method calls – violate formal specifications. Unlike prior RV tools that work event-by-event, TraceMOP tracks monitored traces explicitly. So, TraceMOP can help researchers address several challenges of using RV in testing, e.g., (i) RV overhead is mostly wasted: 99.87% of monitored traces are duplicates of the other 0.13%; and (ii) RV violations are often flaky. We describe TraceMOP’s design, implementation, and plugins for integrating it with Maven projects and GitHub Actions. We evaluate TraceMOP on 105 open-source projects. TraceMOP preserves the monitoring functions of a mature RV tool; it is up to 11x faster and uses up to 231.7GB less memory than our previous prototype. We use TraceMOP to debug four flaky violations; it is open sourced (https://github.com/SoftEngResearch/tracemop) and a demo is at https://youtu.be/xxtUUBlsCJc.
Tue 24 JunDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
10:30 - 12:30 | Verification and ValidationDemonstrations / Ideas, Visions and Reflections / Research Papers / Journal First at Cosmos 3A Chair(s): Alex Orso Georgia Institute of Technology | ||
10:30 10mTalk | TraceMOP: An Explicit-Trace Runtime Verification Tool for Java Demonstrations | ||
10:40 10mTalk | VO-GCSE: Verification Optimization through Global Common Subexpression Elimination Demonstrations Rafael Menezes University of Manchester, Norbert Tihanyi Technology Innovation Institute, Ridhi Jain Technology Innovation Institute (TII), Abu Dhabi, UAE, Alexander Levin Nvidia, Rosiane de Freitas Federal University of Amazonas, Lucas C. Cordeiro University of Manchester, UK and Federal University of Amazonas, Brazil | ||
10:50 10mTalk | GIVUP: Automated Generation and Verification of Textual Process Descriptions Demonstrations Quentin Nivon University Grenoble Alpes, Gwen Salaün University of Grenoble Alpes, Frederic Lang Univ. Grenoble Alpes, Inria, CNRS, Grenoble INP, LIG, Grenoble, France | ||
11:00 10mTalk | NeuroStrata: Harnessing Neuro-Symbolic Paradigms for Improved Testability and Verifiability of Autonomous CPS Ideas, Visions and Reflections Xi Zheng Macquarie University, Ziyang Li University of Pennsylvania, Ivan Ruchkin University of Florida, Ruzica Piskac Yale University, Miroslav Pajic Duke University | ||
11:10 20mTalk | Scene Flow Specifications: Encoding and Monitoring Rich Temporal Safety Properties of Autonomous Systems Research Papers Trey Woodlief University of Virginia, United States, Felipe Toledo , Matthew B Dwyer University of Virginia, Sebastian Elbaum University of Virginia DOI | ||
11:30 20mTalk | QSF: Multi-Objective Optimization based Efficient Solving for Floating-Point Constraints Research Papers Xu Yang College of Computer Science and Technology, National University of Defense Technology, Zhenbang Chen College of Computer, National University of Defense Technology, Wei Dong National University of Defense Technology, Ji Wang National University of Defense Technology DOI | ||
11:50 20mTalk | Consistent Local-First Software: Enforcing Safety and Invariants for Local-First Applications Journal First Mirko Köhler TU Darmstadt, George Zakhour University of St. Gallen, Pascal Weisenburger University of St. Gallen, Guido Salvaneschi University of St. Gallen | ||
12:10 20mTalk | ChangeGuard: Validating Code Changes via Pairwise Learning-Guided Execution Research Papers Lars Gröninger University of Stuttgart, Beatriz Souza Universität Stuttgart, Michael Pradel University of Stuttgart DOI | ||
Cosmos 3A is the first room in the Cosmos 3 wing.
When facing the main Cosmos Hall, access to the Cosmos 3 wing is on the left, close to the stairs. The area is accessed through a large door with the number “3”, which will stay open during the event.