Have you ever tried to verify a program, specified an important property, and then got stuck when the verifier demanded additional specifications to satisfy its prover? 1/8

Our new OOPSLA paper, “Gradual Verification of Recursive Heap Data Structures”, describes a technique that allows programmers to gradually add specifications to the system and stop at any point. 2/8

Gradual Verification checks specifications using a combination of static and dynamic verification. Our paper extends prior Gradual Verification work to more realistic programs with recursive heap data structures (e.g. lists, trees), addressing two technical challenges. 3/8

Similar to recursive types, recursive predicates can be interpreted in two different ways: a predicate’s full recursive unrolling is exposed to the prover (equi-recursive) or it is hidden and must be explicitly unrolled (iso-recursive). 4/8

Iso-recursion is used by static tools, while equi-recursion is natural for dynamic ones. So, our gradual design is consistent across these interpretations! 5/8

Our system allows users to specify heap locations with accessibility predicates, or to delay specification of the heap and rely on the system to check them dynamically. 6/8

Our system verifies accessibility predicates at runtime by tracking and updating a set of owned heap locations. 7/8

To find out more, read our paper https://dl.acm.org/doi/10.1145/3428296. I worked with an amazing team: @olydis, @TheCamdar, @JAldrichCMU, @etanter, @joshsunshine! 8/8