Table of Contents
Conference and Journal Publications
2025
- Place Capability Graphs: A General-Purpose Model of Rust’s Ownership and Borrowing Guarantees pdf
- Zachary Grannan, Aurel Bílý, Jonáš Fiala, Jasper Geer, Markus de Medeiros, Peter Müller, and Alexander J. Summers
- Object-Oriented Programming, Systems, Languages & Applications (OOPSLA) 2025
- Fifteen Years of Viper pdf
- Marco Eilers, Malte Schwerhoff, Alexander J. Summers, and Peter Müller
- Computer Aided Verification (CAV) 2025
- Formal Foundations for Translational Separation Logic Verifiers pdf
- Thibault Dardinier, Michael Sammler, Gaurav Parthasarathy, Alexander J. Summers, and Peter Müller
- Principles of Programming Languages (POPL) 2025
2024
- A Formal Model to Prove Instantiation Termination for E-matching-Based Axiomatisations pdf
- Rui Ge, Ronald Garcia, and Alexander J. Summers
- International Joint Conference on Automated Reasoning (IJCAR) 2024
- Towards Trustworthy Automated Program Verifiers: Formally Validating Translations into an Intermediate Verification Language pdf
- Gaurav Parthasarathy, Thibault Dardinier, Benjamin Bonneau, Peter Müller, and Alexander J. Summers
- Programming Language Design and Implementation (PLDI) 2024
- Reasoning about Interior Mutability in Rust using Library-Defined Capabilities (draft paper) pdf (draft)
- Federico Poli, Xavier Denis, Peter Müller, and Alexander J. Summers
- See also the arxiv version
2023
- Resource Specifications for Resource-Manipulating Programs (draft paper) pdf (draft)
- Zachary Grannan and Alexander J. Summers
- Retrieved from https://arxiv.org/abs/2304.125302024
- Compositional Reasoning for Side-effectful Iterators and Iterator Adapters pdf
- Bı́lỳ Aurel, Jonas Hansen, Peter Müller, and Alexander J Summers
- International Workshop on Aliasing, Capabilities and Ownership (IWACO) 2023
2022
- Fractional Resources in Unbounded Separation Logic pdf
- Thibault Dardinier, Peter Müller, and Alexander J. Summers
- Object-Oriented Programming Systems, Languages, and Applications (OOPSLA) 2022
- Sound Automation of Magic Wands pdf
- Thibault Dardinier, Gaurav Parthasarathy, Noé Weeks, Peter Müller, and Alexander J. Summers
- Computer Aided Verification (CAV) 2022
- The Prusti Project: Formal Verification for Rust pdf
- Vytautas Astrauskas, Aurel Bílý, Jonáš Fiala, Zachary Grannan, Christoph Matheja, Peter Müller, Federico Poli, and Alexander J. Summers
- NASA Formal Methods (NFM) 2022
- REST: Integrating Term Rewriting with Program Verification pdf
- Zachary Grannan, Niki Vazou, Eva Darulova, and Alexander J. Summers
- European Conference on Object-Oriented Programming (ECOOP) 2022
2021
- Modular Specification and Verification of Closures in Rust pdf
- Fabian Wolff, Aurel Bílý, Christoph Matheja, Peter Müller, and Alexander J. Summers
- Object-Oriented Programming Systems, Languages, and Applications (OOPSLA) 2021
- Rich Specifications for Ethereum Smart Contract Verification pdf
- Christian Bräm, Marco Eilers, Peter Müller, Robin Sierra, and Alexander J. Summers
- Object-Oriented Programming Systems, Languages, and Applications (OOPSLA) 2021
- Formally Validating a Practical Verification Condition Generator pdf
- Gaurav Parthasarathy, Peter Müller, and Alexander J. Summers
- Computer Aided Verification (CAV) 2021
2020
- How Do Programmers Use Unsafe Rust? pdf
- Vytautas Astrauskas, Christoph Matheja, Federico Poli, Peter Müller, and Alexander J. Summers
- Object-Oriented Programming Systems, Languages, and Applications (OOPSLA) 2020
- Local Reasoning for Global Graph Properties pdf
- Siddharth Krishna, Alexander J. Summers, and Thomas Wies
- European Symposium on Programming (ESOP) 2020
- Automating Deductive Verification for Weak-Memory Programs (extended version) pdf
- Alexander J. Summers and Peter Müller
- International Journal on Software Tools for Technology Transfer, 2020.
2019
- Leveraging Rust Types for Modular Specification and Verification pdf
- Vytautas Astrauskas, Peter Müller, Federico Poli, and Alexander J. Summers.
- Object-Oriented Programming Systems, Languages, and Applications (OOPSLA) 2019
- Modular Verification of Heap Reachability Properties in Separation Logic pdf
- Arshavir Ter-Gabrielyan, Alexander J. Summers, and Peter Müller
- Object-Oriented Programming Systems, Languages, and Applications (OOPSLA) 2019
- The Axiom Profiler: Understanding and Debugging SMT Quantifier Instantiations pdf
- Nils Becker, Peter Müller, and Alexander J. Summers
- Tools and Algorithms for the Construction and Analysis of Systems (TACAS) 2019
2018
- Permission Inference for Array Programs (extended version) pdf
- Jérôme Dohrau, Alexander J. Summers, Caterina Urban, Severin Münger, and Peter Müller
- Computer Aided Verification (CAV) 2018
- Automating Deductive Verification for Weak-Memory Programs pdf
- Alexander J. Summers and Peter Müller
- Tools and Algorithms for the Construction and Analysis of Systems (TACAS) 2018
- Nominated for Best Paper Award
2016
- Automatic Verification of Iterated Separating Conjunctions using Symbolic Execution pdf
- Peter Müller, Malte Schwerhoff, and Alexander J. Summers
- Computer Aided Verification (CAV) 2016
- Actor Services: Modular Verification of Message Passing Programs pdf
- Alexander J. Summers and Peter Müller
- European Symposium on Programming (ESOP) 2016
- Viper: A Verification Infrastructure for Permission-Based Reasoning pdf
- Peter Müller, Malte Schwerhoff, and Alexander J. Summers
- Verification, Model Checking, and Abstract Interpretation (VMCAI) 2016
2015
- Lightweight Support for Magic Wands in an Automatic Verifier pdf
- Malte Schwerhoff and Alexander J. Summers
- European Conference on Object-Oriented Programming (ECOOP) 2015
2013
- An automatic encoding from VeriFast Predicates into Implicit Dynamic Frames pdf
- Daniel Jost and Alexander J. Summers
- Verified Software: Theories, Tools and Experiments (VSTTE) 2013
- Verification Condition Generation for Permission Logics with Abstract Predicates and Abstraction Functions pdf
- Stefan Heule, Ioannis T. Kassios, Peter Müller, and Alexander J. Summers
- European Conference on Object-Oriented Programming (ECOOP), Springer, 451–476. 2013.
- A Formal Semantics for Isorecursive and Equirecursive State Abstractions pdf
- Alexander J. Summers and Sophia Drossopoulou
- European Conference on Object-Oriented Programming (ECOOP) 2013
- Abstract Read Permissions: Fractional Permissions without the Fractions pdf
- Stefan Heule, K. Rustan M. Leino, Peter Müller, and Alexander J. Summers
- Verification, Model Checking, and Abstract Interpretation (VMCAI) 2013
2012
- The Relationship Between Separation Logic and Implicit Dynamic Frames pdf
- Matthew J. Parkinson and Alexander J. Summers
- Logical Methods in Computer Science, 2012
2011
- Freedom Before Commitment - A Lightweight Type System for Object Initialisation pdf
- Alexander J. Summers and Peter Müller
- Object-Oriented Programming, Systems, Languages and Applications (OOPSLA) 2011
- The Relationship Between Separation Logic and Implicit Dynamic Frames
- Matthew J. Parkinson and Alexander J. Summers
- European Symposium on Programming (ESOP) 2011
2010
- Soundness and Principal Contexts for a Shallow Polymorphic Type System based on Classical Logic pdf
- Alexander J. Summers
- Logic Journal of IGPL, 2010
- Considerate Reasoning and the Composite Design Pattern pdf
- Alexander J. Summers and Sophia Drossopoulou
- Verification, Model Checking, and Abstract Interpretation (VMCAI) 2010
2009
- Curry-Howard Term Calculi for Gentzen-Style Classical Logics pdf
- Alexander J. Summers
- Ph.D. thesis at Imperial College London
- Examined November 2008; awarded Summer 2009
- Universe-Type-Based Verification Techniques for Mutable Static Fields and Methods pdf
- Alexander J. Summers, Sophia Drossopoulou, and Peter Müller
- Journal of Object Technology (JOT), 2009
2008
- Universe Types for Topology and Encapsulation pdf
- David Cunningham, Werner Dietl, Sophia Drossopoulou, Adrian Francalanza, Peter Müller, and Alexander J. Summers
- Formal Methods for Components and Objects (FMCO) 2008
- A Unified Framework for Verification Techniques for Object Invariants pdf
- Sophia Drossopoulou, Adrian Francalanza, Peter Müller, and Alexander J. Summers
- European Conference on Object-Oriented Programming (ECOOP) 2008
2006
- Approaches to Polymorphism in Classical Sequent Calculus pdf
- Alexander J. Summers and Steffen van Bakel
- European Symposium on Programming (ESOP) 2006
Workshop Papers
- Constraint Semantics for Abstract Read Permissions pdf
- John Boyland, Peter Müller, Malte Schwerhoff, and Alexander J. Summers
- Formal Techniques for Java-like Programs (FTfJP) 2014
- Fractional Permissions Without the Fractions pdf
- Stefan Heule, K. Rustan M. Leino, Peter Müller, and Alexander J. Summers
- Formal Techniques for Java-like Programs (FTfJP) 2011
- Size Does Matter: Two Certified Abstractions to Disprove Entailment in Intuitionistic and Classical Separation Logic pdf
- Clément Hurlin, François Bobot, and Alexander J. Summers
- International Workshop on Aliasing, Confinement and Ownership in Object-Oriented Programming (IWACO) 2009
- The Need for Flexible Object Invariants pdf
- Alexander J. Summers, Sophia Drossopoulou, and Peter Müller
- International Workshop on Aliasing, Confinement and Ownership in object-oriented programming (IWACO) 2009
- Modelling Java Requires State pdf
- Alexander J. Summers
- International Workshop on Formal Techniques for Java-like Programs (FTfJP) 2009
- A Universe-Type-Based Verification Technique for Mutable Static Fields and Methods pdf
- Alexander J. Summers, Sophia Drossopoulou, and Peter Müller
- Formal Techniques for Java-like Programs (FTfJP) 2008
- On the Computational Representation of Classical Logical Connectives pdf
- Jayshan Raghunandan and Alexander J. Summers
- International Workshop on Developments in Computational Models (DCM) 2006
Teaching Publications
- Reframing the Liskov Substitution Principle through the Lens of Testing pdf
- Elisa Baniassad and Alexander J. Summers
- ACM SIGPLAN SPLASH-E 2021
- Pandora: A Reasoning Toolbox using Natural Deduction Style pdf
- Krysia Broda, Jiefei Ma, Gabrielle Sinnadurai, and Alexander J. Summers
- Special issue of Logic Journal of the IGPL 2007 on Tools for Teaching Logic
- Pandora - Making Natural Deduction Easy pdf
- Krysia Broda, Jiefei Ma, Gabrielle Sinnadurai, and Alexander J. Summers
- International Congress on Tools for Teaching Logic (ICTTL) 2006
- Friendly e-tutor for Natural Deduction pdf
- Krysia Broda, Jiefei Ma, Gabrielle Sinnadurai, and Alexander J. Summers
- Teaching Formal Methods (TFM) 2006
Selected Technical Reports
- Leveraging Rust Types for Modular Specification and Verification pdf
- Vytautas Astrauskas, Peter Müller, Federico Poli, and Alexander J. Summers
- ETH Zurich, 2018
- Permission Inference for Array Programs (extended version) pdf
- Jérôme Dohrau, Alexander J. Summers, Caterina Urban, Severin Münger, and Peter Müller
- arXiv, 2018
- Viper: A Verification Infrastructure for Permission-Based Reasoning pdf
- Uri Juhasz, Ioannis T. Kassios, Peter Müller, Milos Novacek, Malte Schwerhoff, and Alexander J. Summers
- ETH Zurich, 2014 (separate from the later VMCAI 2016 paper of the same name)