Another key aspect of PyRAT lies in the input partioning mechanisms that it employs. For lower dimensionality inputs, PyRAT is able to use input partioning as a mean to increase the precision of the analysis and prove a wider range of property. This partioning is reinforced by heuristics tailored to the abstract domains we use which allow a significant boost in precision on such networks<br>
Another key aspect of PyRAT lies in the input partitioning mechanisms that it employs. For lower dimensionality inputs, PyRAT is able to use input partitioning as a mean to increase the precision of the analysis and prove a wider range of property. This partitioning is reinforced by heuristics tailored to the abstract domains we use which allow a significant boost in precision on such networks<br>
As an example on the widely used and public benchmark ACAS-XU, PyRAT proves all the defined properties in 292s while state of the art tools such as nnenum takes 319s and neurify 1265s.
