Open project.
Verify brightness property using Deepsymbol.
The Hasse diagram of the dominance relation and the neuron bounds.
Network layers and weights.
Verify infinity norm ball property using Deepsymbol.
Batch verify using Deepsymbol.(Fast Forward)
Import .tf network for ERAN.
Verify infinity norm ball property using ERAN.
Batch verify using ERAN.(Fast Forward)
Find counter-example using PLANET.(Fast Forward)
The counter-example generated.
Run DeepG to generate geometry constraints.(Fast Forward)
Batch verify geometry property using ERAN.(Fast Forward)
Batch verify geometry property using Deepsymbol.(Fast Forward)
Run Reluplex without Deepsymbol.(Fast Forward)
Run Reluplex with Deepsymbol.(Fast Forward)