Authors:

Craig Liu

Date Created:

Not specified

Course Title:

Professor:

Not specified

About Paper:

Static verification is a technique for ensuring software works exactly as intended. It is used in critical software such as control systems for airplanes. However, static verification is arduous and prohibits incrementality, as using it requires writing precise specifications in mathematical logic and all specifications must be written before verification feedback can be received. Gradual verification alleviates these difficulties by allowing incomplete specifications, whose missing parts are then checked dynamically to ensure soundness. The first gradual verifier, Gradual C0, is able to reason about programs that manipulate shared heap memory using permissions. However, Gradual C0's permissions are limited in their expressiveness, as they cannot distinguish between read and write behavior. The ability to do so is important for verifying concurrent programs, since multiple threads often only need to read from the same memory location. To address this, we extend Gradual C0 to support fractional permissions, which associates each heap location with a fraction between zero and one inclusive. If the fraction is nonzero, then it can only be read from, and if it is one, then it can be written to. Arithmetic with the fractions expresses changing between read and write access. We modify Gradual C0's backend verification algorithm to support fractional permissions, adhering to the aforementioned properties. Moving forward, we plan to implement fractional permissions in Gradual C0's specifications and runtime checks. Keywords: Gradual Verification; Fractional Permissions; Separation Logic

Source:

Purdue University / 2024

Topics:

No topics listed

Co-authors:

Craig Liu