NN verification: This work is algorithmically related to NN verification in the context of adversarial robustness. However, adversarial robustness is a local property of the network given a nominal input, and a norm bounded perturbation. Moreover, the robustness property does not consider the notion of sensitive attributes. The NN verification literature is extensive, and the approaches can be grouped into three main groups: (i) SMT-based methods, which encode the problem into a
Satisfiability Modulo Theory problem  [1]}, [2]}, [3]}; (ii) MILP-based solvers,
which solves the verification problem exactly by encoding it as a Mixed Integer Linear
Program  [4]}, [5]}, [6]}, [7]}, [8]}, [9]}, [10]}; (iii) Reachability based methods  [11]}, [12]}, [13]}, [14]}, [15]}, [16]}, [17]}, which perform layer-by-layer reachability analysis to compute a reachable set that can be verified against the property; and (iv) convex
relaxations methods  [18]}, [19]}, [20]}, [21]}, [22]}, [23]}. Generally, (i), (ii), and (iii) do not scale well to large networks. On the other hand, convex relaxation methods use a branch and bound approach to refine the abstraction.
