Ph.D. Program in Software Engineering, Institute for Software Research
Carnegie Mellon University
Gradual Verification of Recursive Heap Data Structures
Static verification tools for recursive heap data structures impose significant annotation burden on developers. This is true even when verifying a simple function that inserts an element at the end of a linked list. Gradual verification was introduced to allow developers to deal with this burden incrementally, if at all. It draws from research on gradual typing to produce a verification system that supports imprecise specifications along a continuum. Our work extends the prior approach to gradual verification to support the specification and verification of programs that use basic recursive data structures like trees or lists. This talk outlines work in progress on this extension and highlights research challenges and proposes solutions to them.