Runtime Verification: 23rd International Conference, RV 2023, Thessaloniki, Greece, October 3–6, 2023, Proceedings (Lecture Notes in Computer Science, 14245)

Preface
Organization
Contents
Invited Papers
Assumption Generation for Learning-Enabled Autonomous Systems
	1 Introduction
	2 Preliminaries
	3 Compositional Verification of Learning-Enabled Autonomous Systems
	4 The TaxiNet System
	5 Evaluation
	6 Related Work
	7 Conclusion
	References
Customizable Reference Runtime Monitoring of Neural Networks Using Resolution Boxes
	1 Introduction
	2 Preliminaries
	3 Boxes with a Resolution
	4 Runtime Monitoring of NNs Using Resolution Boxes
		4.1 Clustering Parameter Selection Using Coverage
		4.2 Monitor Construction
		4.3 Monitor Execution
		4.4 Dealing with Uncertainty Verdicts
	5 Experimental Evaluation
		5.1 Clustering Coverage Estimation
		5.2 Assessing Monitor Precision
		5.3 Discussion and Lessons Learned
	6 Related and Future Work
	References
Regular Papers
Scalable Stochastic Parametric Verification with Stochastic Variational Smoothed Model Checking
	1 Introduction
	2 Background
		2.1 Population Continuous Time Markov Chain
		2.2 Signal Temporal Logic
		2.3 Smoothed Model Checking
	3 Stochastic Variational Smoothed Model Checking
		3.1 Gaussian Processes over Non-Gaussian Likelihoods
		3.2 Bayesian Neural Networks
	4 Experiments
		4.1 Case Studies
		4.2 Experimental Details
		4.3 Experimental Results
	5 Conclusions
		5.1 Statistical Guarantees
	References
Monitoring Blackbox Implementations of Multiparty Session Protocols
	1 Introduction
	2 Networks of Monitored Blackboxes
	3 Monitors for Blackboxes Synthesized from Global Types
	4 Properties of Correct Monitored Blackboxes
		4.1 Satisfaction
		4.2 Soundness
		4.3 Transparency
	5 Conclusion
	References
Mining Specification Parameters for Multi-class Classification
	1 Introduction
	2 Preliminaries
	3 Problem Description
	4 Our Approach
		4.1 Binary Satisfaction
		4.2 Different Templates
		4.3 Multiple Classes
	5 Application
		5.1 Aircraft Elevator
		5.2 Naval Surveillance
		5.3 Parking Scenario
	6 Conclusion and Future Work
	References
General Anticipatory Monitoring for Temporal Logics on Finite Traces
	1 Introduction
	2 Temporal Logics on Finite Traces
		2.1 Temporal Logics and Formalisms on Finite Traces
		2.2 The Stream Runtime Verification Language Lola
	3 Translating TRLTLf to Lola
	4 General Anticipatory Monitoring
		4.1 Recurrent Monitors as Moore Machines
		4.2 An Anticipatory Algorithm
		4.3 Assumptions
		4.4 Uncertainties
	5 Anticipatory Monitoring in Action
	6 Final Remarks
	References
Metric First-Order Temporal Logic with Complex Data Types
	1 Introduction
	2 Design Choices
	3 Complex Data Types
	4 Specification Language
	5 Type System
		5.1 Typing Rules
		5.2 Type Inference
	6 Semantics
	7 Implementation
		7.1 Signature Translation
		7.2 Monitoring Algorithm
	8 Examples and Evaluation
	9 Related Work
	10 Conclusion
	References
Runtime Verification Prediction for Traces with Data
	1 Introduction
	2 Preliminaries
		2.1 Past Time First-Order Temporal Logic
		2.2 Monitoring First-Order Past LTL
		2.3 Predictive Runtime Verification
		2.4 Isomorphism over Relations Representing Qtl Subformulas
	3 Prediction Using BDD Representation
	4 Undecidability of Unbounded Prediction
	5 Experiments
	6 Conclusion
	References
Monitoring Hyperproperties with Prefix Transducers
	1 Introduction
	2 Prefix Expressions
		2.1 Preliminaries
		2.2 Syntax of Prefix Expressions
		2.3 Semantics of Prefix Expressions
	3 Multi-trace Prefix Expressions and Transducers
		3.1 Multi-trace Prefix Expressions
		3.2 Multi-trace Prefix Transducers
	4 Hypertrace Transformations
		4.1 Algorithm for Online Monitoring of k-safety Hyperproperties
		4.2 Discussion
	5 Empirical Evaluation
	6 Related Work
	7 Conclusion and Future Work
	References
Compositional Simulation-Based Analysis of AI-Based Autonomous Systems for Markovian Specifications
	1 Introduction
	2 Motivating Example
	3 Preliminaries
		3.1 Executions and Specifications
		3.2 Markov Decision Processes
	4 Compositional Scenarios
		4.1 Concurrent Hierarchical Probabilistic Extended State Machines
		4.2 Abstract Syntax and Semantics of Compositional Scenarios
	5 Compositional Simulation-Based Analysis
		5.1 Generic Framework
		5.2 Compositional Simulation-Based Falsification
		5.3 Compositional Simulation-Based Statistical Verification
	6 Experimental EvaluationAvailable at https://github.com/BerkeleyLearnVerify/compositional-analysis.
		6.1 An Autonomous Driving Task
		6.2 Evaluation Details
		6.3 Case Study 1
		6.4 Case Study 2
	7 Related Work
	8 Conclusion
	References
Decentralized Predicate Detection Over Partially Synchronous Continuous-Time Signals
	1 Introduction: Detecting All Errors in Distributed CPS
	2 Preliminaries and Problem Definition
		2.1 The Continuous-Time Setup
		2.2 Problem Definition: Decentralized Predicate Detection
	3 The Structure of Satisfying Cuts
	4 The Abstractor Process
		4.1 Physical Vector Clocks
		4.2 Abstractor Description
	5 The Slicer Process for Detecting Predicates
		5.1 Worked-Out Example
	6 Case Studies and Evaluation
	7 Conclusion
	References
Flexible Runtime Security Enforcement with Tagged C
	1 Introduction
	2 Metadata Tags and Policies, by Example
	3 The Tagged C Language: Syntax and Semantics
	4 Example Policies
		4.1 Memory Safety
		4.2 Compartmentalization
		4.3 Secure Information Flow
	5 Implementation
	6 Related Work
	7 Conclusion and Future Work
	References
Pattern Matching for Perception Streams
	1 Introduction
	2 Preliminaries
		2.1 Perception Stream
	3 Spatial Regular Expressions
	4 Perception Stream Matching
		4.1 Problem Formulation
		4.2 Spatio-Temporal Regular Expression Matcher
	5 Examples and Benchmarks
		5.1 Example A: Offline Matching Examples
		5.2 Example B: Online Matching
		5.3 Benchmarks
	6 Related Work
	7 Conclusion and Future Work
	References
Learning Monitor Ensembles for Operational Design Domains
	1 Introduction
	2 Monitorable Operational Design Domains
		2.1 Monitorable Operational Design Domains
		2.2 Challenges in Learning Optimal ODDs
	3 Learning Monitor Ensembles for Operational Design Domains
		3.1 Using Majority Voting
		3.2 Using Multi-armed Bandits
	4 Empirical Study
		4.1 Case Study
		4.2 Framework and Implementation
		4.3 Evaluation
		4.4 Experiment: Majority Voting
		4.5 Experiment: Multi-armed Bandit
	5 Related Work
	6 Conclusion
	References
Monitoring Algorithmic Fairness Under Partial Observations
	1 Introduction
		1.1 Related Work
	2 Preliminaries
		2.1 Notation
		2.2 Randomized Event Generators: Partially Observed Markov Chains
		2.3 Register Monitors
	3 Monitoring Quantitative Algorithmic Fairness Properties
		3.1 Role of the Stationary Distribution
		3.2 Bounded Specification Expressions
		3.3 Problem Statement
	4 Construction of the Monitor
		4.1 A Point Estimator for the Atoms
		4.2 The Atomic Monitor
		4.3 The Complete Monitor
	5 Experiments
	6 Conclusion
	References
Short and Tool Papers
AMT: A Runtime Verification Tool of Video Streams
	1 Introduction
	2 Approach Overview
	3 Property Specification Using AML
	4 Software Architecture
	5 Experiments and Results
	6 Related Work
	7 Conclusion
	References
Bridging the Gap: A Focused DSL for RV-Oriented Instrumentation with BISM
	1 Introduction
	2 DSL Design Considerations
	3 BISM Background
	4 The DSL for BISM
		4.1 Pointcuts
		4.2 Events
		4.3 Monitors
		4.4 Code Generation
	5 Implementation
	6 Evaluation
		6.1 Performance Evaluation
		6.2 User Experience Evaluation
	7 Related Work and Conclusion
	References
CCMOP: A Runtime Verification Tool for C/C++ Programs
	1 Introduction
	2 Framework
	3 Design and Implementation
	4 Evaluation
	5 Related Work
	6 Conclusion and Future Work
	References
A Stream Runtime Verification Tool with Nested and Retroactive Parametrization
	1 Introduction
	2 Overview
	3 HLola with Dynamic Parametrization
	4 A Network Traffic Case Study and Empirical Evaluation
	5 Conclusions
	References
eMOP: A Maven Plugin for Evolution-Aware Runtime Verification
	1 Introduction
	2 eMOP
		2.1 Evolution-Aware RV Techniques
		2.2 Implementation
	3 Installation and Usage
	4 Evaluation
	5 Conclusions and Future Work
	References
Runtime Monitoring of Accidents in Driving Recordings with Multi-type Logic in Empirical Models
	1 Introduction
	2 Related Work
	3 Motivating Study
		3.1 Analysis on High-Level Time-Series Abstraction
		3.2 Analysis on Discontinuity of Anomaly Detection
	4 Proposed Method
		4.1 High-Level Time-Series Feature Extraction
		4.2 Empirical Model for Accident Classification
		4.3 Logic Calibration and Verification
	5 Evaluation Results
		5.1 Evaluation Setup
		5.2 Baselines
		5.3 Evaluation of Model Performance
	6 Conclusion
	References
Safety Monitoring for Pedestrian Detection in Adverse Conditions
	1 Introduction
	2 Preliminaries
		2.1 IA-YOLO
		2.2 Timed Quality Temporal Logic (TQTL)
	3 Our Approach
	4 Experimental Analysis
	5 Conclusion
	References
Tutorials
Instrumentation for RV: From Basic Monitoring to Advanced Use Cases
	1 Introduction
	2 Understanding Instrumentation
		2.1 Unveiling the Complete Picture
		2.2 Observing the Execution
		2.3 Instrumentation for Runtime Verification
		2.4 Instrumentation Considerations for Runtime Verification
	3 Instrumentation Requirements
	4 How to Evaluate Instrumentation
	5 Existing Instrumentation Frameworks
		5.1 Bytecode Manipulation Libraries
		5.2 Aspect Oriented Languages
		5.3 The Gap Between Bytecode Libraries and AOP Frameworks
	6 A Comprehensive Instrumentation Approach: BISM
		6.1 Instrumentation Model
		6.2 Instrumentation Language
	7 Insrumentation Use Cases
		7.1 Classical Example
		7.2 Residual Runtime Verification
		7.3 Runtime Verification of Concurrent Programs
		7.4 Opportunistic Monitoring
		7.5 Control Flow Integrity
	8 Conclusion
	References
Runtime Monitoring DNN-Based Perception
	1 Introduction
	2 Challenges in Monitoring Perception Systems
	3 Formulation
	4 Techniques
		4.1 DNN Monitoring Techniques from the ML Community
		4.2 DNN Monitoring Techniques from the FM Community
		4.3 Monitoring Techniques Without Analyzing the DNN
	5 Challenges Ahead
	References
Monitorability for Runtime Verification
	1 Introduction
	2 Preliminaries
		2.1 Runtime Verification
		2.2 Linear Temporal Logic
	3 Monitorability
		3.1 Characterizing Temporal Properties According to Monitorability
		3.2 Runtime Verification Algorithms for Monitorability
		3.3 A Lower Bound Example for LTL Monitoring
	4 Monitoring Safety Properties
		4.1 Past Propositional Temporal Logic
		4.2 RV for Propositional Past Time LTL
		4.3 From Monitoring Past Property  to Monitoring
		4.4 From Monitoring Propositional to First Order Temporal Logic
	References
Learning-Based Approaches to Predictive Monitoring with Conformal Statistical Guarantees
	1 Introduction
	2 Background
		2.1 Signal Temporal Logic (STL)
	3 Predictive Monitoring
	4 Uncertainty Estimation and Statistical Guarantees
		4.1 Conformal Inference
		4.2 Bayesian Inference
	5 Learning-Based PM with Statistical Guarantees
		5.1 Monitoring Under Full Observability
		5.2 Monitoring Under Partial Observability
		5.3 Uncertainty-Aware Error Detection and Active Learning
	6 Related Work
	7 Conclusions
	References
Author Index