Dear all:
We computed the reachable set for the nonlinear van der pol oscillator with C2E2 and wanted to share our results:
- The initial set is given by x in [1.25,1.55] and y in [2.35,2.45]
- The unsafe set if given by y>=2.75
C2E2 is able to verify the model after 64 refinements. However, since the unsafe set does not bound the x dimension, the x dimension bloats up quickly in our case.
The result for variable x,y is provided below and a model file from C2E2 is attached below.
The 3rd International Competition on Verifying Continuous and Hybrid Systems (ARCH-COMP'19) held as a part of the 6th International Workshop on Applied Verification for Continuous and Hybrid Systems (ARCH'19) occurred on April 15, 2019 as a part of the ACM/IEEE Cyber-Physical Systems and Internet-of-Things Week (CPS-IoT Week).