REASONING OVER STRINGS AND OTHER UNBOUNDED DATA STRUCTURES

Abstract

Data structures play a central role in software development. While developing proper data structures is not easy, reasoning about them is even harder. The difficulty comes from their typical characteristic: the unboundedness of the data structures and/or the loops manipulating them. This makes two following fundamental issues more severe: inter-dependence between structures and data values, and complicated interactions between different data structures. In this thesis, we consider the problem of reasoning about unbounded data structures such as strings, linked lists, trees. Specifically, we propose systematic techniques for the satisfiability problem of string constraints, and the entailment proving problem for heap-allocated data structures. These two problems are of great interest: for example, while the former is important for security analysis of web applications, the latter is important for automated verification of imperative programs.