Current static verification techniques do not provide good support for incre- mentality, 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 recur sive, 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 present- ing 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 scalability 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. 143 pages

Thesis Committee:
Jonathan Aldrich (Co-Chair)
Joshua Sunshine (Co-Chair)
Bryan Parno
Éric Tanter (University of Chile)
Peter Müller (ETH Zurich)

James D. Herbsleb, Head, Software and Societal Systems Department
Martial Hebert, Dean, School of Computer Science

Return to: SCS Technical Report Collection
School of Computer Science

This page maintained by reports@cs.cmu.edu