Table of Contents
In March 2020 I joined the Department of Computer Science at the University of British Columbia, as an Associate Professor. I'm looking for strong PhD, MSc and internship students to work with on a broad variety of topics connected to program correctness (see below).
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 year, 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.
A (possibly reasonably up-to-date) CV is available here.
Papers
2020
- How Do Programmers Use Unsafe Rust? Pdf (draft)
- Local Reasoning for Global Graph Properties Pdf (draft, on arxiv)
- To appear at ESOP 2020
- Automating deductive verification for weak-memory programs (extended version) Pdf
- In STTT Special Issue of extended selected papers from TACAS 2018
2019
- Leveraging Rust Types for Modular Specification and Verification Pdf
- Presented at OOPSLA 2019
- Modular Verification of Heap Reachability Properties in Separation Logic Pdf
- Presented at OOPSLA 2019
- The Axiom Profiler: Understanding and Debugging SMT Quantifier Instantiations Pdf
- Nils Becker and Peter Müller and Alexander J. Summers
- Presented at TACAS 2019
2018
- Permission Inference for Array Programs Pdf (extended)
- Presented at CAV 2018
- Automating Deductive Verification for Weak-Memory Programs Pdf [Extended version]
- Presented at TACAS 2018
- Nominated for Best Paper Award
2016
2015
- Software Verification “Across the Stack” Pdf
- Invited Dahl-Nygaard Junior Prize talk and abstract for ECOOP 2015
- See also the recording (YouTube)
- Lightweight Support for Magic Wands in an Automatic Verifier Pdf
- Presented at ECOOP 2015
2014
- Constraint Semantics for Abstract Read Permissions Pdf
- Presented at FTfJP 2014
- Viper: A Verifi cation Infrastructure for Permission-Based Reasoning Pdf
2013
- A Formal Semantics for Isorecursive and Equirecursive State Abstractions Pdf
- Presented at ECOOP 2013
- Verification Condition Generation for Permission Logics with Abstract Predicates and Abstraction Functions Pdf
- Presented at ECOOP 2013
- An automatic encoding from VeriFast Predicates into Implicit Dynamic Frames Pdf
- Daniel Jost and Alexander J. Summers
- Presented at VSTTE 2013
- Abstract Read Permissions: Fractional Permissions without the Fractions Pdf
- Presented at VMCAI 2013
2012
- The Relationship Between Separation Logic and Implicit Dynamic Frames Pdf
- Much expanded and improved, based on ESOP 2011 paper below (Pdf)
- Published in Logical Methods in Computer Science
2011
- Freedom Before Commitment - A Lightweight Type System for Object Initialisation Pdf
- Presented at OOPSLA/SPLASH 2011
- see also the (slightly outdated) Technical Report (Jan 2011), ETH Zurich
- Fractional Permissions Without the Fractions Pdf
- Presented at FTfJP 2011
- see also the slides (pptx)
- The Relationship Between Separation Logic and Implicit Dynamic Frames Pdf
- Presented at ESOP 2011
- see also the follow-on LMCS 2012 paper above (Pdf)
- see also the slides (pptx)
2010
- Towards a Semantic Model for Wildcards Pdf
- Presented at FTfJP 2010
- See also the slides (ppt)
- Considerate Reasoning and the Composite Design Pattern Pdf
- Presented at VMCAI 2010
- See also the Boogie2 code (zip)
- Soundness and Principal Contexts for a Shallow Polymorphic Type System based on Classical Logic Pdf
2009
- The Need for Flexible Object Invariants Pdf
- Presented at IWACO 2009
- Modelling Java Requires State Pdf
- Presented at FTfJP 2009
- Universe-Type-Based Verification Techniques for Mutable Static Fields and Methods Pdf
- Size Does Matter: Two Certified Abstractions to Disprove Entailment in Intuitionistic and Classical Separation Logic Pdf
- Presented at IWACO 2009
2008
- A Universe-Type-Based Verification Technique for Mutable Static Fields and Methods Pdf
- Presented at FTfJP 2008
- See also the extended version (also above)
- A Unified Framework for Verification Techniques for Object Invariants Pdf
- Presented at ECOOP 2008
- See also the full version (submitted)
- Universe Types for Topology and Encapsulation Pdf
- Published in LNCS: Post-proceedings FMCO 2007
- Curry-Howard Term Calculi for Gentzen-Style Classical Logics (PhD Thesis) Pdf
- First supervisor : Steffen van Bakel
- Second supervisor: Luca Cardelli.
2007
- Pandora: A Reasoning Toolbox using Natural Deduction Style Pdf
2006
- On the Computational Representation of Classical Logical Connectives Pdf
- Presented at DCM 2006, Published in ENTCS special issue
- See also the slides
- Approaches to Polymorphism in Classical Sequent Calculus Pdf
- Presented at ESOP 2006
- Pandora - Natural Deduction made Easy Pdf
- Presented at ICTTL 2006
Selected Talks
- The Relationship Between Separation Logic and Implicit Dynamic Frames slides (pptx) (pdf)
- Invited talk at Imperial College London (extension of presentation at ESOP 2011)
- Based on joint work with Matthew Parkinson
- (See also the paper (pdf))
- Natural Delimited Control: A Curry-Howard Correspondence for a Canonical Classical Natural Deduction slides (ppt)
- Invited talk at the British Logic Colloquium 2009
- (See also my thesis, Chapters 5 and 6)
- On the Computational Representation of Classical Logical Connectives slides(ppt)