Authors:

Priyam Gupta

Date Created:

Not specified

Course Title:

Professor:

Not specified

About Paper:

Current static verification tools provide unmatched guarantees about code, however, they burden users with the task of writing complete and complex specifications. Gradual verification eases this burden by combining static (compile time) and dynamic (run time) verification techniques to support the incremental specification and verification of code. Gradual C0 is the first practicable gradual verifier for realistic heap-manipulating programs, allowing users to write incomplete specifications and providing earlier feedback with run-time checks. However, Gradual C0 currently lacks support for certain constructs, making it less expressive than its underlying static verifier, Viper. In particular, it lacks expressibility in specifying relationships amongst nodes in recursive heap data structures like trees and lists, which are fundamental constructs widely used in software development for efficient data management. Because of this limitation, users have to come up with complex roundabout solutions for specifying properties such as the sortedness of a linked list or a binary search tree. This paper details the design for implementation of Viper's unfolding expressions in Gradual C0 that will increase its specifications' expressibility. The design maintains Gradual C0's efficiency and minimizes run time checks by preserving heap information where possible during evaluation of these expressions. Support for unfolding expressions will pave the way for adding pure functions to Gradual C0 which will bring the verifier's expressibility very close to current static verifiers like Viper, making verification technology more usable and mainstream. Keywords: Gradual Verification; Implicit Dynamic Frames; Recursive Predicates; Viper

Source:

Purdue University / 2024

Topics:

No topics listed

Co-authors:

Priyam Gupta