| 2025 | CAV | Fifteen Years of Viper. | Marco Eilers, Malte Schwerhoff, Alexander J. Summers, Peter Mller |
| 2024 | IJCAR | A Formal Model to Prove Instantiation Termination for E-matching-Based Axiomatisations. | Rui Ge, Ronald Garcia, Alexander J. Summers |
| 2022 | CAV | Sound Automation of Magic Wands. | Thibault Dardinier, Gaurav Parthasarathy, No Weeks, Peter Mller, Alexander J. Summers |
| 2022 | ECOOP | REST: Integrating Term Rewriting with Program Verification. | Zachary Grannan, Niki Vazou, Eva Darulova, Alexander J. Summers |
| 2021 | CAV | Formally Validating a Practical Verification Condition Generator. | Gaurav Parthasarathy, Peter Mller, Alexander J. Summers |
| 2021 | OOPSLA | Reframing the Liskov substitution principle through the lens of testing. | Elisa L. A. Baniassad, Alexander J. Summers |
| 2020 | ECOOP | Prusti: deductive verification for Rust (keynote). | Alexander J. Summers |
| 2020 | ESOP | Local Reasoning for Global Graph Properties. | Siddharth Krishna, Alexander J. Summers, Thomas Wies |
| 2019 | TACAS | The Axiom Profiler: Understanding and Debugging SMT Quantifier Instantiations. | Nils Becker, Peter Mller, Alexander J. Summers |
| 2018 | CAV | Permission Inference for Array Programs. | Jrme Dohrau, Alexander J. Summers, Caterina Urban, Severin Mnger, Peter Mller |
| 2018 | TACAS | Automating Deductive Verification for Weak-Memory Programs. | Alexander J. Summers, Peter Mller |
| 2016 | CAV | Automatic Verification of Iterated Separating Conjunctions Using Symbolic Execution. | Peter Mller, Malte Schwerhoff, Alexander J. Summers |
| 2016 | ESOP | Actor Services - Modular Verification of Message Passing Programs. | Alexander J. Summers, Peter Mller |
| 2016 | VMCAI | Viper: A Verification Infrastructure for Permission-Based Reasoning. | Peter Mller, Malte Schwerhoff, Alexander J. Summers |
| 2015 | ECOOP | Lightweight Support for Magic Wands in an Automatic Verifier. | Malte Schwerhoff, Alexander J. Summers |
| 2015 | ECOOP | Software Verification "Across the Stack" (Invited Talk). | Alexander J. Summers |
| 2014 | ECOOP | Constraint Semantics for Abstract Read Permissions. | John Tang Boyland, Peter Mller, Malte Schwerhoff, Alexander J. Summers |
| 2013 | ECOOP | Verification Condition Generation for Permission Logics with Abstract Predicates and Abstraction Functions. | Stefan Heule, Ioannis T. Kassios, Peter Mller, Alexander J. Summers |
| 2013 | ECOOP | A Formal Semantics for Isorecursive and Equirecursive State Abstractions. | Alexander J. Summers, Sophia Drossopoulou |
| 2013 | VMCAI | Abstract Read Permissions: Fractional Permissions without the Fractions. | Stefan Heule, K. Rustan M. Leino, Peter Mller, Alexander J. Summers |
| 2011 | ECOOP | Fractional permissions without the fractions. | Stefan Heule, K. Rustan M. Leino, Peter Mller, Alexander J. Summers |
| 2011 | ESOP | The Relationship between Separation Logic and Implicit Dynamic Frames. | Matthew J. Parkinson, Alexander J. Summers |
| 2011 | OOPSLA | Freedom before commitment: a lightweight type system for object initialisation. | Alexander J. Summers, Peter Mller |
| 2010 | ECOOP | Towards a semantic model for Java wildcards. | Alexander J. Summers, Nicholas Cameron, Mariangiola Dezani-Ciancaglini, Sophia Drossopoulou |
| 2010 | VMCAI | Considerate Reasoning and the Composite Design Pattern. | Alexander J. Summers, Sophia Drossopoulou |
| 2009 | ECOOP | Modelling Java requires state. | Alexander J. Summers |
| 2008 | ECOOP | A Unified Framework for Verification Techniques for Object Invariants. | Sophia Drossopoulou, Adrian Francalanza, Peter Mller, Alexander J. Summers |
| 2006 | ESOP | Approaches to Polymorphism in Classical Sequent Calculus. | Alexander J. Summers, Steffen van Bakel |