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

Session Chair: Thomas Ferrère (teaser) (zoom)

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:

  • Vivian M. Ho, Chris Alvin, Supratik Mukhopadhyay and Jimmie Lawson: Empirical Abstraction
  • Niraj Basnet and Houssam Abbas: Logical Signal Processing: A Fourier Analysis of Temporal Logic
  • Nastaran Shafiei, Klaus Havelund and Peter Mehlitz: Actor-based Runtime Verification with MESA
10:50-11:00 Closing Remarks