Authors:

Doruk Alp Mutlu

Date Created:

Not specified

Course Title:

Professor:

Not specified

About Paper:

Static program verification is a crucial process in software development, particularly for safety-critical systems. Unfortunately, static verification tools require precise and complete program specifications from users, which is burdensome and slows down the verification process. Gradual verification eases the software verification process by seamlessly combining static verification and dynamic verification allowing imprecise (partial) specifications. The only sound implementation of a gradual verification system is Gradual C0, which targets the C0 programming language (a safe subset of C). Gradual C0 supports recursive heap data structures such as linked lists, trees, etc. However, Gradual C0's specification language is lacking in expressibility, missing key features such as pure functions and quantifiers. Extending Gradual C0 with pure functions allows specifications on the values stored in data structures while hiding implementation details. To address these limitations of Gradual C0, we introduce pure functions to Gradual C0. First, we provide formal rules for pure functions in Gradual C0's Intermediate Verification language. Then, we plan to implement these changes in Gradual C0. Our design follows from the design of Viper, also using an axiomatization strategy as part of the pure function verification. Extending Gradual C0 with pure functions will allow rich functional specifications. Future work will explore the extension of Gradual C0 with quantifiers and a soundness proof for both extensions. Keywords: Gradual Verification; Static Verification; Pure Functions; Implicit Dynamic Frames

Source:

Purdue University / 2025

Topics:

No topics listed

Co-authors:

Doruk Alp Mutlu