2 papers
cs.PL2026
Gradually Verifying Unfolding Expressions & Pure Functions
Hazel Torek, Long Tien Nguyen, Priyam Gupta +2
Unfolding expressions, which temporarily unfold a predicate to leverage its owned fields when evaluating a heap-dependent expression, and pure functions, which are heap-dependent f…
cs.PL2025
Increasing the Expressiveness of a Gradual Verifier
Priyam Gupta
Static verification provides strong correctness guarantees for code; however, fully specifying programs for static verification is a complex, burdensome process for users. Gradual…