Learning Abstractions for Verifying Data-Structure Properties

This paper concerns the question of how to create abstractions that are useful for program analysis. It presents a method that refines an abstraction automatically for analysis problems in which the semantics of statements and the query of interest are expressed using logical formulas. We present two strategies for refining an abstraction. The simpler strategy is effective in many cases. The second strategy uses a known machine-learning algorithm to learn an appropriate abstraction. A tool that incorporates the method has been implemented and applied to several programs that manipulate linked lists and binary-search trees. In all cases, the tool is able to demonstrate (i) the partial correctness of the programs, and (ii) that the programs possess additional properties---e.g., stability or antistability