Empirical Abstraction

Given a program analysis problem that consists of a program and a property of interest, we use an empirical approach to automatically construct a sequence of abstractions that approach an ideal abstraction suitable for solving that problem. This process begins with an infinite concrete domain that maps to a finite abstract cluster domain defined by statistical procedures. Given a set of properties expressed as formulas in a restricted and bounded variant of CTL, we can test the success of the abstraction with respect to a predefined performance measure. In addition, we can perform iterative abstraction-refinement of the clustering by tuning hyperparameters that determine the accuracy of the cluster representations (abstract states) and determine the number of clusters