Alexander Summers

Associate Professor

Research Interests

programming languages
software engineering

Relevant Thesis-Based Degree Programs


Graduate Student Supervision

Master's Student Supervision

Theses completed in 2010 or later are listed below. Please note that there is a 6-12 month delay to add the latest theses.

Simpler specifications for resource-manipulating programs (2023)

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


If this is your researcher profile you can log in to the Faculty & Staff portal to update your details and provide recruitment preferences.


Sign up for an information session to connect with students, advisors and faculty from across UBC and gain application advice and insight.