Program Verification via Three-Valued Logic Analysis
8Software errors cost the US economy billions of dollars each year. According to reasonable estimates, a third of the cost can be saved through the use of enhanced tools for software quality. My dissertation addresses a key challenge in software verification: how to analyze programs that perform destructive manipulation of linked (or recursive) data structures. I applied the concept of abstraction refinement to the problem of automating shape analysis, static analysis that establishes properties of such programs. My thesis exposed a new connection between Machine Learning and program analysis--in particular, that Inductive Logic Programming (ILP) provides a key primitive for abstraction refinement. The techniques developed in my thesis have been implemented as extensions to the Three-Valued Logic Analysis tool, or TVLA. They allowed the automatic verification of a number of interesting properties of programs that destructively manipulate singly- and doubly-linked lists, binary trees, and binary-search trees.