Gradual verification, which combines static verification with dynamic checks to verify programs with partial specifications, was introduced to reduce the disadvantages of either static or dynamic program verification in isolation. There is an existing implementation of a gradual verifier for the C0 subset of the C programming language, built as a frontend for the Viper verification infrastructure, and a corresponding proof of soundness. However, many features from static deductive verification still have not yet been implemented or formalized in the gradual setting.

Unfolding expressions, which temporarily unfold a predicate to frame a heap-dependent expression with ownership of additional fields, present a challenge because of how gradual verification blends isorecursive and equirecursive semantics. We expand upon the formalization of gradual verification by providing the static and dynamic semantics for unfolding expressions as well as ongoing updates to the proof of soundness. Our extension of the proof will apply to any verifier that uses the Viper verification infrastructure, and we therefore anticipate having the first proof of soundness including unfolding expressions in an implicit dynamic frames-based verifier, static or gradual.