PV2 UDDERgenerates a bounded version of the given unbounded verification problem

Reduces the unbounded verification problem of Delay Differential Equations (DDEs) to a bounded problem.

Application domain/field

Internals

They focus on verifying safety properties of delayed dynamical systems encoded by Delay Differential Equations (DDEs), where safety properties pertain to an infinite domain. They present a quantitative method to construct estimations. This reduces the temporally unbounded verification problem to a bounded one. Implemented in Wolfram Mathematica. Uses DDE-BIFTOOL.

Comments

It is called a "prototypical implementation" in the CAV '19 paper.

Links

Download page: http://lcs.ios.ac.cn/~chenms/tools/

Last commit date

12 May 2019

Related papers

https://doi.org/10.1007/978-3-030-25540-4_37 (CAV 2019)

Last publication date

12 July 2019

ProVerB specific

View/edit source (Markdown)



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