Gradual Verification of Recursive Heap Data Structures

 Current static verification techniques do not provide good support for incrementality, making it difficult for developers to focus on specifying and verifying the properties and components that are most important. Dynamic verification approaches support incrementality, but cannot provide static guarantees. To bridge this gap, prior work proposed gradual verification, which supports incrementality by allowing every assertion to be complete, partial, or omitted, and provides sound verification that smoothly scales from dynamic to static checking. While promising, the prior approach to gradual verification is merely an indication of feasibility in a very simple setting and is limited to programs without recursive heap data structures. 

This dissertation extends gradual verification to programs that manipulate recursive, mutable data structures on the heap. It lays the formal foundations for such gradual verification systems, addressing several technical challenges, such as semantically connecting iso- and equi-recursive interpretations of abstract predicates, and supporting gradual verification of heap ownership.

 This work demonstrates the practicality of these foundations by first presenting Gradual C0, the first working gradual verifier for recursive heap data structures. Gradual C0 targets C0, a safe subset of C designed for education. During Gradual C0’s development, technical challenges related to symbolic execution with imprecise specifications, minimizing insertion of dynamic checks, and extensibility to other programming languages beyond C0 were addressed. Next, I present an empirical study of gradual verification technology, which explores how specification precision correlates with run-time checking in Gradual C0. The results show that on average, Gradual C0 decreases run-time overhead between 11-34% compared to dynamic verification alone. Further, run-time performance increases in Gradual C0 as more specifications are written—and proof obligations are introduced but not statically verified—until reaching a critical mass where afterwards performance decreases correspondingly—as more and more proof obligations are proved statically. Finally, I also present a case study exploring Gradual C0’s practicability and scala?bility by using the tool to verify a 3k lines of code C parser for loop termination. I found that Gradual C0’s strong adherence to the gradual guarantee—which ensures Gradual C0 does not produce static or dynamic verification errors resulting from missing specifications—was necessary for assuring real software with many modules and functions and allowed me to find bugs in code and specifications far earlier than static verification alone. However, this property at times hindered efforts to reduce run-time checking through writing additional specifications. I propose a new specification construct (inspired by prior work in gradual typing) that is designed to facilitate this process in the presence of the gradual guarantee. 

This dissertation thus makes significant contributions to realizing the promising idea of gradual verification, and lays a solid foundation for future gradual verification technology and tools that work at scale