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

Format:

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.

Internals

This framework includes:

Comments

License: MIT
Automaton

Links

Last commit date

1 October 2021

Related papers

https://doi.org/10.1007/978-3-319-63387-9_22 (CAV '17)

Last publication date

13 July 2017

ProVerB specific

View/edit source (Markdown)



ProVerB is a part of SLEBoK. Last updated: July 2022.