Alexander Summers

Many program verifiers allow specifications to be written in terms of program states. The specification language of a program verifier is typically a superset of the source language, extended with additional constructs such as first-order quantifiers. This is a pragmatic choice because it allows the same language to be used for both implementation and specification. This kind of language is ideal for properties that can be easily expressed in terms of program expressions.However, programs that manipulate resources, such as money, are best described in terms of how they operate on resources rather than in terms of program state. This is because properties that are implicit when reasoning about resources must be made explicit in specifications written using program expressions. As a result, specifications of resource-manipulating programs tend to be complex, are difficult to compose, and are hard for non-experts to understand.In this thesis, we present a methodology for extending a modular program verifier to support resource reasoning in its specifications. Users can specify where resources are created and destroyed, and assert properties about the resource state. The verifier ensures that resource operations cannot fail, and that the asserted properties hold.Our methodology does not require first-class support for resources in the source language itself, and does not impose requirements on how resources are represented in the program. Instead, users can define coupling invariants to relate changes in the resource state to changes in the program state; these invariants are enforced by the verifier. Coupling invariants enable simpler specifications because they enable users to describe changes in program state in terms of resource operations.We implement our methodology as an extension to the Prusti program verifier. To evaluate our technique, we use our extended version of Prusti to verify properties of a real-world blockchain application. We show that, compared to a more-classical specification implemented without resource reasoning, our methodology enables more concise specifications.

View record