Approaches to Polymorphism in Classical Sequent Calculus. - Alexander J. Summers; Steffen van Bakel (ESOP, 2006)

On the Computational Representation of Classical Logical Connectives. - Jayshan Raghunandan; Alexander J. Summers (DCM@ICALP, 2006)

Universe Types for Topology and Encapsulation. - Dave Cunningham; Werner Dietl; Sophia Drossopoulou; Adrian Francalanza; Peter Müller 001; Alexander J. Summers (FMCO, 2007)

Pandora: A Reasoning Toolbox using Natural Deduction Style. - Krysia Broda; Jiefei Ma; Gabrielle Sinnadurai; Alexander J. Summers (Log. J. IGPL, 2007)

A Unified Framework for Verification Techniques for Object Invariants. - Sophia Drossopoulou; Adrian Francalanza; Peter Müller 001; Alexander J. Summers (Types, Logics and Semantics for State, 2008)

Curry-Howard Term Calculi for Gentzen-Style Classical Logics. - Alexander J. Summers (2008)

Modelling Java requires state. - Alexander J. Summers (FTfJP@ECOOP, 2009)

Universe-Type-Based Verification Techniques for Mutable Static Fields and Methods. - Alexander J. Summers; Sophia Drossopoulou; Peter Müller 001 (J. Object Technol., 2009)

Towards a semantic model for Java wildcards. - Alexander J. Summers; Nicholas Cameron 001; Mariangiola Dezani-Ciancaglini; Sophia Drossopoulou (FTfJP@ECOOP, 2010)

Considerate Reasoning and the Composite Design Pattern. - Alexander J. Summers; Sophia Drossopoulou (VMCAI, 2010)

Fractional permissions without the fractions. - Stefan Heule; K. Rustan M. Leino; Peter Müller 001; Alexander J. Summers (FTfJP@ECOOP, 2011)

Freedom before commitment: a lightweight type system for object initialisation. - Alexander J. Summers; Peter Müller 001 (OOPSLA, 2011)

Soundness and principal contexts for a shallow polymorphic type system based on classical logic. - Alexander J. Summers (Log. J. IGPL, 2011)

The Relationship Between Separation Logic and Implicit Dynamic Frames - Matthew J. Parkinson; Alexander J. Summers (Log. Methods Comput. Sci., 2012)

Verification Condition Generation for Permission Logics with Abstract Predicates and Abstraction Functions. - Stefan Heule; Ioannis T. Kassios; Peter Müller 001; Alexander J. Summers (ECOOP, 2013)

A Formal Semantics for Isorecursive and Equirecursive State Abstractions. - Alexander J. Summers; Sophia Drossopoulou (ECOOP, 2013)

Abstract Read Permissions: Fractional Permissions without the Fractions. - Stefan Heule; K. Rustan M. Leino; Peter Müller 001; Alexander J. Summers (VMCAI, 2013)

An Automatic Encoding from VeriFast Predicates into Implicit Dynamic Frames. - Daniel Jost 001; Alexander J. Summers (VSTTE, 2013)

Constraint Semantics for Abstract Read Permissions. - John Tang Boyland; Peter Müller 001; Malte Schwerhoff; Alexander J. Summers (FTfJP@ECOOP, 2014)

Lightweight Support for Magic Wands in an Automatic Verifier. - Malte Schwerhoff; Alexander J. Summers (ECOOP, 2015)

Software Verification "Across the Stack" (Invited Talk). - Alexander J. Summers (ECOOP, 2015)

Lightweight Support for Magic Wands in an Automatic Verifier (Artifact). - Malte Schwerhoff; Alexander J. Summers (Dagstuhl Artifacts Ser., 2015)

Automatic Verification of Iterated Separating Conjunctions Using Symbolic Execution. - Peter Müller 001; Malte Schwerhoff; Alexander J. Summers (CAV (1), 2016)

Actor Services - Modular Verification of Message Passing Programs. - Alexander J. Summers; Peter Müller 001 (ESOP, 2016)

Viper: A Verification Infrastructure for Permission-Based Reasoning. - Peter Müller 001; Malte Schwerhoff; Alexander J. Summers (VMCAI, 2016)

Viper: A Verification Infrastructure for Permission-Based Reasoning. - Peter Müller 001; Malte Schwerhoff; Alexander J. Summers (Dependable Software Systems Engineering, 2017)

Permission Inference for Array Programs. - Jérôme Dohrau; Alexander J. Summers; Caterina Urban; Severin Münger; Peter Müller 001 (CAV (2), 2018)

Automating Deductive Verification for Weak-Memory Programs. - Alexander J. Summers; Peter Müller 001 (TACAS (1), 2018)

The Axiom Profiler: Understanding and Debugging SMT Quantifier Instantiations. - Nils Becker; Peter Müller 001; Alexander J. Summers (TACAS (1), 2019)

Leveraging rust types for modular specification and verification. - Vytautas Astrauskas; Peter Müller 001; Federico Poli 001; Alexander J. Summers (Proc. ACM Program. Lang., 2019)

Modular verification of heap reachability properties in separation logic. - Arshavir Ter-Gabrielyan; Alexander J. Summers; Peter Müller 001 (Proc. ACM Program. Lang., 2019)

Prusti: deductive verification for Rust (keynote). - Alexander J. Summers (FTfJP@ECOOP, 2020)

Local Reasoning for Global Graph Properties. - Siddharth Krishna 001; Alexander J. Summers; Thomas Wies (ESOP, 2020)

How do programmers use unsafe rust? - Vytautas Astrauskas; Christoph Matheja; Federico Poli 001; Peter Müller 001; Alexander J. Summers (Proc. ACM Program. Lang., 2020)

Automating deductive verification for weak-memory programs (extended version). - Alexander J. Summers; Peter Müller 001 (Int. J. Softw. Tools Technol. Transf., 2020)

Formally Validating a Practical Verification Condition Generator. - Gaurav Parthasarathy; Peter Müller 001; Alexander J. Summers (CAV (2), 2021)

Reframing the Liskov substitution principle through the lens of testing. - Elisa L. A. Baniassad; Alexander J. Summers (SPLASH-E, 2021)

Modular Verification of Collaborating Smart Contracts. - Christian Bräm; Marco Eilers; Peter Müller 001; Robin Sierra; Alexander J. Summers (CoRR, 2021)

Formally Validating a Practical Verification Condition Generator (extended version). - Gaurav Parthasarathy; Peter Müller 001; Alexander J. Summers (CoRR, 2021)

Rich specifications for Ethereum smart contract verification. - Christian Bräm; Marco Eilers; Peter Müller 001; Robin Sierra; Alexander J. Summers (Proc. ACM Program. Lang., 2021)

Modular specification and verification of closures in Rust. - Fabian Wolff; Aurel Bílý; Christoph Matheja; Peter Müller 001; Alexander J. Summers (Proc. ACM Program. Lang., 2021)

Improving Linear Separability of Pulse Wave Laser Additive Manufacturing Classifiers with Rational Feature Engineering and Selection *. - Alexander J. Summers; Houshang Yin; Ralf D. Fischer; Barton C. Prorok; Xiaoyuan Lou; Q. Peter He (ACC, 2022)

Sound Automation of Magic Wands. - Thibault Dardinier; Gaurav Parthasarathy; Noé Weeks; Peter Müller 001; Alexander J. Summers (CAV (2), 2022)

REST: Integrating Term Rewriting with Program Verification. - Zachary Grannan; Niki Vazou; Eva Darulova; Alexander J. Summers (ECOOP, 2022)

The Prusti Project: Formal Verification for Rust. - Vytautas Astrauskas; Aurel Bílý; Jonás Fiala; Zachary Grannan; Christoph Matheja; Peter Müller 001; Federico Poli 001; Alexander J. Summers (NFM, 2022)

REST: Integrating Term Rewriting with Program Verification (Extended Version). - Zachary Grannan; Niki Vazou; Eva Darulova; Alexander J. Summers (CoRR, 2022)

Sound Automation of Magic Wands (extended version). - Thibault Dardinier; Gaurav Parthasarathy; Noé Weeks; Alexander J. Summers; Peter Müller 001 (CoRR, 2022)

Compositional Reasoning for Side-effectful Iterators and Iterator Adapters. - Aurel Bílý; Jonas Hansen; Peter Müller 001; Alexander J. Summers (CoRR, 2022)

REST: Integrating Term Rewriting with Program Verification (Artifact). - Zachary Grannan; Niki Vazou; Eva Darulova; Alexander J. Summers (Dagstuhl Artifacts Ser., 2022)

Fractional resources in unbounded separation logic. - Thibault Dardinier; Peter Müller 001; Alexander J. Summers (Proc. ACM Program. Lang., 2022)

Resource Specifications for Resource-Manipulating Programs. - Zachary Grannan; Alexander J. Summers (CoRR, 2023)

A Formal Model to Prove Instantiation Termination for E-matching-Based Axiomatisations. - Rui Ge 001; Ronald Garcia; Alexander J. Summers (IJCAR (1), 2024)

Towards Trustworthy Automated Program Verifiers: Formally Validating Translations into an Intermediate Verification Language (extended version). - Gaurav Parthasarathy; Thibault Dardinier; Benjamin Bonneau; Peter Müller 001; Alexander J. Summers (CoRR, 2024)

A Formal Model to Prove Instantiation Termination for E-matching-Based Axiomatisations (Extended Version). - Rui Ge 001; Ronald Garcia; Alexander J. Summers (CoRR, 2024)

Reasoning about Interior Mutability in Rust using Library-Defined Capabilities. - Federico Poli 001; Xavier Denis; Peter Müller 001; Alexander J. Summers (CoRR, 2024)

Formal Foundations for Translational Separation Logic Verifiers (extended version). - Thibault Dardinier; Michael Sammler; Gaurav Parthasarathy; Alexander J. Summers; Peter Müller 001 (CoRR, 2024)

Towards Trustworthy Automated Program Verifiers: Formally Validating Translations into an Intermediate Verification Language. - Gaurav Parthasarathy; Thibault Dardinier; Benjamin Bonneau; Peter Müller 001; Alexander J. Summers (Proc. ACM Program. Lang., 2024)

Fifteen Years of Viper. - Marco Eilers; Malte Schwerhoff; Alexander J. Summers; Peter Müller 001 (CAV (1), 2025)

Formal Foundations for Translational Separation Logic Verifiers. - Thibault Dardinier; Michael Sammler; Gaurav Parthasarathy; Alexander J. Summers; Peter Müller 001 (Proc. ACM Program. Lang., 2025)

Place Capability Graphs: A General-Purpose Model of Rust's Ownership and Borrowing Guarantees. - Zachary Grannan; Aurel Bílý; Jonás Fiala; Jasper Geer; Markus de Medeiros; Peter Müller 001; Alexander J. Summers (CoRR, 2025)