  We propose a symbolic representation for support vector machines (SVMs) by
means of abstract interpretation, a well-known and successful technique for
designing and implementing static program analyses. We leverage this
abstraction in two ways: (1) to enhance the interpretability of SVMs by
deriving a novel feature importance measure, called abstract feature importance
(AFI), that does not depend in any way on a given dataset of the accuracy of
the SVM and is very fast to compute, and (2) for verifying stability, notably
individual fairness, of SVMs and producing concrete counterexamples when the
verification fails. We implemented our approach and we empirically demonstrated
its effectiveness on SVMs based on linear and non-linear (polynomial and radial
basis function) kernels. Our experimental results show that, independently of
the accuracy of the SVM, our AFI measure correlates much more strongly with the
stability of the SVM to feature perturbations than feature importance measures
widely available in machine learning software such as permutation feature
importance. It thus gives better insight into the trustworthiness of SVMs.
