Gradual verification supports partial specifications by soundly applying static checking where possible and dynamic checking when necessary. This approach supports incrementality and provides a formal guarantee of verifiability. The first gradual verifier, Gradual C0, supports programs that manipulate recursive, mutable data structures on the heap and minimizes dynamic checks with statically available information. However, the current approach for evaluating these dynamic checks is naive during incremental specificity. There is a re-assertion of dynamic checks for all imprecise logic, even if these formulas might share the same trace path. In this paper, we introduce an optimization pipeline for identifying and minimizing these common traces. We accomplish this by treating all iso-recursive predicates as equi-recursive at runtime. To not break the soundness of Gradual񐶰, we do not make any changes to the semantic evaluation of the static verifier. Instead, we preserve the evaluation of iso-recursive predicates statically, and carry this information into Gradual C0’s Gradual Viper intermediate representation. By unrolling all static predicates as if they were dynamic checks, we are able to correlate when the naive dynamic checks from the optimistic IR overlap. This allows us to perform a more sophisticated predicate equivalence matching using the Z3 SMT solver. We suggest that the lazy treatment of static specifications at the source-level is more in line with the incremental philosophy of gradual verification, and better supports more complex dynamic checks. We show the effectiveness on our benchmarks of tree data structures. We also raise the question of synthesizing intermediate predicates to bridge partial predicate matching.

I’m an undergrad @ Cornell University working towards computer science and philosophy degrees. My main research goals involve developing practical tools for software verification in general and domain-specific cases through programming language theory.