PV4 DryVRproduces a satisfiability/reachability result for a hybrid control system

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.

Application domain/field

Expected input


JSON file (this used to be a text file in the earlier versions of DryVR)

Expected output

Safe or Unsafe? Any reachtubes or counterexamples are also stored in text files.


This framework includes:


License: MIT
Automaton Hybrid system


Related papers

DryVR: Data-Driven Verification and Compositional Reasoning for Automotive Systems (CAV '17)

Last publication date

13 July 2017

ProVerB specific

ProVerB is a part of SLEBoK. Last updated: February 2023.