Demonstrators

Demonstrators posted as YouTube videos

In this very short video (as supplementary material for the IV'20 paper), we demonstrate the performance between a DNN trained using provably robust training techniques (as proposed in the paper) and a DNN training using standard techniques.
As an example, by separately applying single-step FGSM attacks on two networks with the same attack intensity (the actual attacks are different), one can observe that, for standard DNN that predicts the centre-of-lane, the output prediction can greatly vary. This does not happen for the provably robust training network.

FESTO demonstrator with automatic occupancy check, face detection with error handling, and object storing by color. The executable code is first by synthesizing the PDDL-like FESTO model, followed by using a script to automatically translate each atomic action to corresponding hardware control actions. Details can be found in MGSyn

Execute the automatically synthesized controller program on CODESYS soft PLC. Details can be found in G4LTL-ST

Perform formal verification to find adversarial images and to formally secure highway motion predictors trained from NGSim dataset. Details can be found in our ATVA'17 paper

Use autoCode4 to synthesize actor-based controllers from formal specification represented in linear temporal logic. The working environment is Ptolemy II, an open-source tool for engineering cyber-physical systems.

Google Sites

Report abuse