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

• Delay Differential Equations (DDEs)
• Dynamical systems
• Safety verification

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.