UC Riverside

Data structures are one of the most important part of programming. Program faults lead to

corruption of runtime data structures of the program which lead to program failure or worse wrong output. Such kind of bugs are hard to debug using traditional debugging techniques. Specification based debugging techniques have been useful in solving such bugs with limited effectiveness. Debugging is one of the most costly part of software development process both in terms of time and man-power. On the other hand, verification compliments debugging

by providing guarantee of correctness. Therefore, automatic debugging and verification

techniques greatly increase the productivity of the programmer. This dissertation concentrates on the techniques for debugging and verification of data-structures. Firstly, we propose an efficient and precise fault location framework for single threaded application. The framework includes a compact memory graph representation to store data structure evolution history, a specification language for user to simply specify data structure constraints and a precise fault location method. Secondly, we propose a linearizability verification technique for concurrent data-structures. Our verification technique is both sound and generic. We are able to verify

more concurrent data structures linearizable than any other state of the art linearizability

verication technique.