The program is given in Pacific Daylight Time (PDT)!
Day 0: October 6, Tutorials Day | ||||
6:30-8:30 |
Invited Tutorial: L. Nenzi, E. Bartocci, L. Bortolussi, M. Loreti, E. Visconti, Monitoring Spatio-Temporal Properties |
|||
8:30-8:45 | Break | |||
8:45-10:45 |
Tutorial 1 Session Chair: Yliès Falcone |
Tutorial 2 Session Chair: Houssam Abbas |
Tutorial 3 Session Chair: Dmitriy Traytel |
Tutorial 4 Session Chair: Nicolas Basset |
Tutorial 1: Y. A. Liu and S. D. Stoller Assurance of Distributed Algorithms and Systems: Runtime Checking of Safety and Liveness (teaser) (video) (zoom) Tutorial 2: M. Schwenger, Monitoring Cyber-Physical Systems from Design to Integration (teaser) (video) (zoom) Tutorial 3: J. H. Dawes, M. Han, O. Javed, G. Reger, G. Franzoni, A. Pfeiffer, Analysing the Performance of Python-based Web Services with the VyPR Framework (teaser) (video) (zoom) Tutorial 4: K. Havelund, D. Peled, BDDs for Representing Data in Runtime Verification (teaser) (video) (zoom) (NEW TIME: 11:00-13:00 PDT) |
||||
10:45-11:00 | Break (zoom) | |||
11:00-11:45 | Tutorials Q&A | |||
Day 1: October 7, RV for Software Systems | ||||
Session 1: Keynote Session, Chair: Jyo Deshmukh | ||||
6:45-7:00 | Opening Remarks, Logistics | |||
7:00-8:00 | Keynote: Lane Desborough, The Physical Side of Cyber-Physical Systems (zoom) | |||
8:00-8:10 | Break (zoom) | |||
Session 2: Software Monitoring, Chair: Bernd Finkbeiner (teasers) (zoom) | ||||
8:10-8:30 | V. M. Ho, C. Alvin, S. Mukhopadhyay and J. Lawson. Empirical Abstraction | |||
8:30-8:50 | B. Maderbacher, A. F. Karl and R. Bloem. Placement of Runtime Checks to Counteract Fault Injections | |||
8:50-9:10 | D. Basin, M. Gras, S. Krstic and J. Schneider. Scalable Online Monitoring of Distributed Systems | |||
9:10-9:30 | M. Guzman, O. Riganelli, D. Micucci and L. Mariani. Test4Enforcers: Test Case Generation for Software Enforcers | |||
9:30-9:40 | Break (zoom) | |||
Session 3: RV for software systems: short papers, Chair: Borzoo Bonakdarpour (teasers) (zoom) | ||||
9:40-9:55 | A. Cizmarik and P. Parizek. SharpDetect: Dynamic Analysis Framework for C#/.NET Programs | |||
9:55-10:10 | N. Kosmatov, F. Maurica and J. Signoles. Efficient Runtime Assertion Checking of Properties over Mathematical Numbers | |||
10:10-10:25 | C. Soueidi, A. Kassem and Y. Falcone. BISM: Bytecode-Level Instrumentation for Software Monitoring | |||
10:25-10:35 | Break (zoom) | |||
Session 4: Cyber-Physical Systems Chair: Maximilian Schwenger (teasers) (zoom) | ||||
10:35-10:55 | A. Tibo, M. Jaeger and K. Larsen. From Statistical Model Checking to Run-Time Monitoring using a Bayesian Network Approach | |||
10:55-11:15 | S. Wu, C. Bai, K. Chang, Y. Hsieh, C. Huang, C. Lin, E. Kang, and Q. Zhu. Efficient System Verification with Multiple Weakly-Hard Constraints for Runtime Monitoring | |||
11:15-11:20 | Poster: Isaac Mackey and Jianwen Su. Service Provisioning with Verification Techniques | |||
Day 2: October 8, Temporal Logic, Stream-based Monitoring | ||||
Session 5: Keynote Session. Chair: Dejan Nickovic | ||||
7:00-8:00 | Keynote: Thomas Henzinger, Monitorability under Assumptions (zoom) | |||
8:00-8:10 | RV 2021 Announcement | |||
Session 6: Stream-based Monitoring, Chair: Hazem Torfah (teasers) (zoom) | ||||
8:10-8:30 | B. Finkbeiner, S. Oswald, N. Passing and Maximilian Schwenger. Verified Rust Monitors for Lola Specifications | |||
8:30-8:50 | F. Gorostiaga, L. Miguel Danielsson and C. Sanchéz. Unifying the Time-Event Spectrum for Stream Runtime Verification | |||
8:50-9:05 | S. Krstic and J. Schneider. A Benchmark Generator for Online First-Order Monitoring | |||
9:05-9:20 | J. Baumeister, B. Finkbeiner, M. Kruse and M. Schwenger. Automatic Optimizations for Stream-based Specification Languages | |||
9:20-9:30 | Break (zoom) | |||
Session 7: Temporal Logic, Chair: Stefan Jaksic (teasers) (zoom) | ||||
9:30-9:50 | N. Basnet and H. Abbas. Logical Signal Processing: A Fourier Analysis of Temporal Logic | |||
9:50-10:10 | T. Wright and I. Stark. Property-Directed Verified Monitoring of Signal Temporal Logic | |||
10:10-10:30 | A. Chattopadhyay and K. Mamouras. A Verified Online Monitor for Metric Temporal Logic with Quantitative Semantics | |||
10:30-10:45 | E. Bartocci, L. Bortolussi, M. Loreti, L. Nenzi and S. Silvetti. MoonLight: A Lightweight Tool for Monitoring Spatio-Temporal Properties | |||
10:45-11:00 | J. Cralley, O. Spantidi, B. Hoxha and G. Fainekos. TLTk: A Toolbox for Parallel Robustness Computation of Temporal Logic Specifications | |||
11:00-11:20 | Business Meeting | |||
Day 3: October 9, RV for Autonomy | ||||
Session 8: Keynote Session. Chair: Ezio Bartocci | ||||
7:00-8:00 | Keynote: Katherine Driggs-Campbell. Fantastic Failures and Where to Find Them: Designing Trustworthy Autonomy (zoom) | |||
8:00-8:10 | Break (zoom) | |||
Session 9: Panel Discussion on RV for autonomy. Moderators: Dejan Nickovic & Jyo Deshmukh (zoom) | ||||
8:10-9:10 | Panel on RV for Autonomy – Panelists:
Nathan Aschbacher – Auxon Mauricio Castillo-Effen – Lockheed Martin Katherine Driggs-Campbell – University of Illinois at Urbana-Champaign Jens Oehlerking – Robert Bosch GmbH Aditya Zutshi – Galois |
|||
9:10-9:15 | Break (zoom) | |||
Session 10: RV for autonomy papers. Chair: Oleg Sokolsky (teasers) (zoom) | ||||
9:15-9:35 | N. Shafiei, K. Havelund and P. Mehlitz. Actor-based Runtime Verification with MESA | |||
9:35-9:55 | W. Zhou, R. Gao, E. Kang, B. Kim and W. Li. Runtime-Safety-Guided Policy Repair | |||
9:55-10:15 | M. Yahyazadeh, S. Rafiul Hussain, E. Hoque and O. Chowdhury. PatrIoT: Policy Assisted Resilient Programmable IoT System | |||
10:15-10:30 | Eleni Zapridou, Ezio Bartocci and Panagiotis Katsaros. Runtime Verification of Autonomous Driving Systems in CARLA | |||
10:30-10:45 | S. Shivakumar, H. Torfah, A. Desai and S. A. Seshia. SOTER on ROS: A Run-Time Assurance Framework on the Robot Operating System | |||
10:45-10:50 |
Best Paper and Test of Time Awards Announcement Best paper nominees:
|
|||
10:50-11:00 | Closing Remarks |