Benchmark for formal methods for characterization and safety

The objective of this activity is to compare tools in order to recommend the most relevant for spe-cific use case. The evaluation of tools is performed according to several metrics related essentiallyto the complexity of the tool and its performance.The evaluation is performed on two use cases: ACAS Xu and the Renault welding images. How-ever for technical reasons, we are unable to fully evaluate the robustness of the welding modelswith all tools. These technical reasons include the high dimension of welding images and thecomplex architecture of the decision model (composed of several layers). For this reason, wepropose to consider public benchmarks such as CIFAR instead. We take advantage of mentioningthat a robustness optimization activity on large dimension data has been launched in the programin 2022.