A non-convex classifier support for abstraction-refinement framework

The main challenge of the counterexample guided abstraction/refinement model checking is the separation of real and spurious counterexamples. This goal is achieved by the classification. In this paper, we reduce the complexity of classification by targeting the problem of feature selection for a considered data set. To do so, we develop a Support Vector Machine (SVM) extended by a Smoothly Clipped Absolute Deviation (SCAD) penalty, to improve the classification scalability by selecting the most important features. The obtained model leads to solve a non-convex optimization problem. The latter is solved by a successive linear programming algorithm with finite convergence. Preliminary computational experiments on different benchmarks demonstrate that our methods accomplish the desired goal of selecting the most important features with a minimum error.