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. It draws from research on gradual typing to produce a verification system that supports imprecise specifications along a continuum. However, current gradual verification technology can only support a simple first-order specification logic. This paper outlines an extension to gradual verification that supports implicit dynamic frames and recursive abstract predicates through an example and highlighted challenges and solutions to developing this extension. This extension is a significant step toward making verification technology more usable and cost effective in practice, ultimately leading to higher quality software.

Research Advisor: Jonathan Aldrich

ACM Student Member Number: 8215205

Category: Graduate