Proving Data Structure Properties by Automatic Induction

Minh-Thai Trinh, Duc-Hiep Chu and Joxan Jaffar


We consider the problem of reasoning over an expressive constraint language for unbounded strings. The difficulty comes from recursively defined functions such as replace, making state-of-the-art algorithms non-terminating. Our first contribution is a progressive search algorithm to not only mitigate the problem of non-terminating reasoning but also guide the search towards a minimal solution when the input formula is in fact satisfiable. We have implemented our method using the state-of-the-art Z3 framework. Importantly, we have en- abled conflict clause learning for string theory so that our solver can be used effectively in the setting of program verification. Finally, our experimental evalu- ation shows leadership in a large benchmark suite, and a first deployment for an- other benchmark suite which requires reasoning about string formulas of a class that has not been solved before.