alex.jpgWelcome to my home page. As an academic on paper, I go by the alias Alexander J. Summers, but in other capacities you can call me Alex.

In March 2020 I joined the Department of Computer Science at the University of British Columbia (UBC), as an Associate Professor. I'm looking for strong postdocs, PhD, MSc and internship students to work with on a broad variety of topics connected to program correctness (see below). Prior to coming to UBC I worked at ETH Zürich as a senior researcher (Deutsch: Oberassistent II), in the Chair of Programming Methodology group run by Peter Müller.

I work in the general area of program correctness, including developing new specification and verification logics and type systems, and developing automated tools for constructing proofs about heap-based and concurrent programs, usually building on SMT solvers. For many years, I co-ordinated the Viper Project, in which we develop a new intermediate verification language and tool suite designed to ease the construction of new verification tools for modern reasoning techniques.

I recently started the Prusti Project, in which we are building the first deductive verification tools for the Rust programming language. More generally, I mainly work in the area of software verification for concurrent and object-oriented programs, and I'm delighted to have been awarded the 2015 Dahl-Nygaard Junior Prize for my work in this area. This was awarded at ECOOP 2015. More information about my research can be found here.

Some personal (but not too personal) things can be found here, and if you need to contact me (feel free), my email address is alex dot summers at ubc dot ca