Runtime Verification: 20th International Conference, RV 2020, Los Angeles, CA, USA, October 6–9, 2020, Proceedings (Programming and Software Engineering Book 12399)

This book constitutes the refereed proceedings of the 20th International Conference on Runtime Verification, RV 2020, held in Los Angeles, CA, USA, in October 2020. The conference was held virtually due to the COVID-19 pandemic. The 14 regular papers and 2 short papers presented in this book were carefully reviewed and selected from 43 submissions. Also included are an invited paper, 5 tutorial papers, 6 tool papers, and a benchmark paper. The RV conference is concerned with all aspects of monitoring and analysis of hardware, software and more general system executions. The papers are organized in the following topical sections: runtime verification for autonomy; runtime verification for software; runtime verification with temporal logic specifications; stream-based monitoring; and runtime verification for cyber-physical systems. Front Matter ....Pages i-xix Front Matter ....Pages 1-1 Monitorability Under Assumptions (Thomas A. Henzinger, N. Ege Saraç)....Pages 3-18 Front Matter ....Pages 19-19 Monitoring Spatio-Temporal Properties (Invited Tutorial) (Laura Nenzi, Ezio Bartocci, Luca Bortolussi, Michele Loreti, Ennio Visconti)....Pages 21-46 Assurance of Distributed Algorithms and Systems: Runtime Checking of Safety and Liveness (Yanhong A. Liu, Scott D. Stoller)....Pages 47-66 Analysing the Performance of Python-Based Web Services with the VyPR Framework (Joshua Heneage Dawes, Marta Han, Omar Javed, Giles Reger, Giovanni Franzoni, Andreas Pfeiffer)....Pages 67-86 Monitoring Cyber-Physical Systems: From Design to Integration (Maximilian Schwenger)....Pages 87-106 BDDs for Representing Data in Runtime Verification (Klaus Havelund, Doron Peled)....Pages 107-128 Front Matter ....Pages 129-129 Runtime-Safety-Guided Policy Repair (Weichao Zhou, Ruihan Gao, BaekGyu Kim, Eunsuk Kang, Wenchao Li)....Pages 131-150 PatrIoT: Policy Assisted Resilient Programmable IoT System (Moosa Yahyazadeh, Syed Rafiul Hussain, Endadul Hoque, Omar Chowdhury)....Pages 151-171 Runtime Verification of Autonomous Driving Systems in CARLA (Eleni Zapridou, Ezio Bartocci, Panagiotis Katsaros)....Pages 172-183 SOTER on ROS: A Run-Time Assurance Framework on the Robot Operating System (Sumukh Shivakumar, Hazem Torfah, Ankush Desai, Sanjit A. Seshia)....Pages 184-194 Front Matter ....Pages 195-195 Scalable Online Monitoring of Distributed Systems (David Basin, Matthieu Gras, Srđan Krstić, Joshua Schneider)....Pages 197-220 Actor-Based Runtime Verification with MESA (Nastaran Shafiei, Klaus Havelund, Peter Mehlitz)....Pages 221-240 Placement of Runtime Checks to Counteract Fault Injections (Benedikt Maderbacher, Anja F. Karl, Roderick Bloem)....Pages 241-258 Empirical Abstraction (Vivian M. Ho, Chris Alvin, Supratik Mukhopadhyay, Brian Peterson, Jimmie D. Lawson)....Pages 259-278 Test4Enforcers: Test Case Generation for Software Enforcers (Michell Guzman, Oliviero Riganelli, Daniela Micucci, Leonardo Mariani)....Pages 279-297 SharpDetect: Dynamic Analysis Framework for C#/.NET Programs (Andrej Čižmárik, Pavel Parízek)....Pages 298-309 Efficient Runtime Assertion Checking for Properties over Mathematical Numbers (Nikolai Kosmatov, Fonenantsoa Maurica, Julien Signoles)....Pages 310-322 BISM: Bytecode-Level Instrumentation for Software Monitoring (Chukri Soueidi, Ali Kassem, Yliès Falcone)....Pages 323-335 Front Matter ....Pages 337-337 Property-Directed Verified Monitoring of Signal Temporal Logic (Thomas Wright, Ian Stark)....Pages 339-358 Logical Signal Processing: A Fourier Analysis of Temporal Logic (Niraj Basnet, Houssam Abbas)....Pages 359-382 A Verified Online Monitor for Metric Temporal Logic with Quantitative Semantics (Agnishom Chattopadhyay, Konstantinos Mamouras)....Pages 383-403 TLTk: A Toolbox for Parallel Robustness Computation of Temporal Logic Specifications (Joseph Cralley, Ourania Spantidi, Bardh Hoxha, Georgios Fainekos)....Pages 404-416 MoonLight: A Lightweight Tool for Monitoring Spatio-Temporal Properties (Ezio Bartocci, Luca Bortolussi, Michele Loreti, Laura Nenzi, Simone Silvetti)....Pages 417-428 Front Matter ....Pages 429-429 Verified Rust Monitors for Lola Specifications (Bernd Finkbeiner, Stefan Oswald, Noemi Passing, Maximilian Schwenger)....Pages 431-450 Automatic Optimizations for Stream-Based Monitoring Languages (Jan Baumeister, Bernd Finkbeiner, Matthis Kruse, Maximilian Schwenger)....Pages 451-461 Unifying the Time-Event Spectrum for Stream Runtime Verification (Felipe Gorostiaga, Luis Miguel Danielsson, César Sánchez)....Pages 462-481 A Benchmark Generator for Online First-Order Monitoring (Srđan Krstić, Joshua Schneider)....Pages 482-494 Front Matter ....Pages 495-495 Efficient System Verification with Multiple Weakly-Hard Constraints for Runtime Monitoring (Shih-Lun Wu, Ching-Yuan Bai, Kai-Chieh Chang, Yi-Ting Hsieh, Chao Huang, Chung-Wei Lin et al.)....Pages 497-516 From Statistical Model Checking to Run-Time Monitoring Using a Bayesian Network Approach (Manfred Jaeger, Kim G. Larsen, Alessandro Tibo)....Pages 517-535 Back Matter ....Pages 537-538