Design of Fractional Permissions for a Gradual Verifier

Static verification assures program correctness but requires heavy user annotation. Gradual verification alleviates this burden by allowing users to write partial, imprecise specifications that are checked statically where possible and dynamically when necessary. The first gradual verifier, Gradual C0, reasons about shared heap memory through a permission logic. This paper describes an extension to Gradual C0 which supports fractional permissions in its permission logic.