# DRYVR:Data-driven verification and compositional reasoning for automotive systems

arXiv: https://arxiv.org/abs/1702.06902 · HTML: https://mlsanity.com/paper/1702.06902/

## Key facts

- Cited by 14 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 22 Feb 2017.

## Built on by (most cited first, 14 of 14)

- [Data-Driven Reachability Analysis of Stochastic Dynamical Systems with Conformal Inference](https://mlsanity.com/paper/2309.09187/) (2023)
- [Symbolic Abstractions From Data: A PAC Learning Approach](https://mlsanity.com/paper/2104.13901/) (2021)
- [Formal Verification of Unknown Dynamical Systems via Gaussian Process Regression](https://mlsanity.com/paper/2201.00655/) (2021)
- [Bridging Dimensions: Confident Reachability for High-Dimensional Controllers](https://mlsanity.com/paper/2311.04843/) (2023)
- [Statistical Reachability Analysis of Stochastic Cyber-Physical Systems under Distribution Shift](https://mlsanity.com/paper/2407.11609/) (2024)
- [Quokka: Accelerating Program Verification with LLMs via Invariant Synthesis](https://mlsanity.com/paper/2509.21629/) (2025)
- [Data-Driven Reachability analysis and Support set Estimation with Christoffel Functions](https://mlsanity.com/paper/2112.09995/) (2021)
- [Refining Perception Contracts: Case Studies in Vision-based Safe Auto-landing](https://mlsanity.com/paper/2311.08652/) (2023)
- [NExG: Provable and Guided State Space Exploration of Neural Network Control Systems using Sensitivity Approximation](https://mlsanity.com/paper/2207.03884/) (2022)
- [Taming Reachability Analysis of DNN-Controlled Systems via Abstraction-Based Training](https://mlsanity.com/paper/2211.11127/) (2022)
- [Certifying Safety in Reinforcement Learning under Adversarial Perturbation Attacks](https://mlsanity.com/paper/2212.14115/) (2022)
- [Data-Driven Falsification of Cyber-Physical Systems](https://mlsanity.com/paper/2505.03863/) (2025)
- [Conformal Reachability for Safe Control in Unknown Environments](https://mlsanity.com/paper/2602.03799/) (2026)
- [Correcting Learning-based Perception for Safety](https://mlsanity.com/paper/2609.22108/) (2026)

## Abstract (arXiv)

We present the DRYVR framework for verifying hybrid control systems that are described by a combination of a black-box simulator for trajectories and a white-box transition graph specifying mode switches. The framework includes (a) a probabilistic algorithm for learning sensitivity of the continuous trajectories from simulation data, (b) a bounded reachability analysis algorithm that uses the learned sensitivity, and (c) reasoning techniques based on simulation relations and sequential composition, that enable verification of complex systems under long switching sequences, from the reachability analysis of a simpler system under shorter sequences. We demonstrate the utility of the framework by verifying a suite of automotive benchmarks that include powertrain control, automatic transmission, and several autonomous and ADAS features like automatic emergency braking, lane-merge, and auto-passing controllers.