UC San Diego

Because every aspect of our lives is now inexorably dependent on software, it is crucial that the software systems that we depend on are reliable, safe, and correct. However, verifying that software systems are safe and correct in the real world is extraordinarily difficult. In this dissertation, we posit that this difficulty is often due to a fundamental impedance mismatch between a programmer's "high-level" intent for the operation of their program versus the "low-level" source code that they write. In particular, we claim that the impedance exists in the large because of the lack of mechanisms available for encoding and verifying complex properties of unbounded data structures. Then, we propose several augmentations of the Liquid Types method of automatic program verification for uniformly describing high-level specifications and for verifying that source code is correct with respect to such specifications. First, we describe a means of verifying the correctness of programs that perform subtle manipulations over complex recursive and linked data structures such as sorted lists, balanced trees and acyclic graphs. Second, we describe a means of verifying the correctness of concurrent, shared memory programs that perform subtle manipulations on the heap. In particular we automatically verify that concurrent, heap manipulating programs intended to be deterministic over all possible schedules do always produce the same heap. Finally, we show empirically that these techniques are practical and efficient by building two tools: DSolve, for verifying that real programs that manipulate complex data structures do so correctly, and CSolve for verifying that real, subtly deterministic heap manipulating programs do, in fact, always produce the same heap.