Alexander J. Summers

ORCID

Publication Activity (10 Years)

Years Active: 2006-2024
Publications (10 Years): 39

Top Venues

CoRR

Proc. ACM Program. Lang.

CAV (2)

ECOOP

Imperial College London, UK (PHD)

Education History

Imperial College London, UK

PHD

Publications

Rui Ge, Ronald Garcia, Alexander J. Summers
A Formal Model to Prove Instantiation Termination for E-matching-Based Axiomatisations (Extended Version). CoRR (2024)
Gaurav Parthasarathy, Thibault Dardinier, Benjamin Bonneau, Peter Müller, Alexander J. Summers
Towards Trustworthy Automated Program Verifiers: Formally Validating Translations into an Intermediate Verification Language (extended version). CoRR (2024)
Gaurav Parthasarathy, Thibault Dardinier, Benjamin Bonneau, Peter Müller, Alexander J. Summers
Towards Trustworthy Automated Program Verifiers: Formally Validating Translations into an Intermediate Verification Language. Proc. ACM Program. Lang. 8 (PLDI) (2024)
Rui Ge, Ronald Garcia, Alexander J. Summers
A Formal Model to Prove Instantiation Termination for E-matching-Based Axiomatisations. IJCAR (1) (2024)
Federico Poli, Xavier Denis, Peter Müller, Alexander J. Summers
Reasoning about Interior Mutability in Rust using Library-Defined Capabilities. CoRR (2024)
Thibault Dardinier, Michael Sammler, Gaurav Parthasarathy, Alexander J. Summers, Peter Müller
Formal Foundations for Translational Separation Logic Verifiers (extended version). CoRR (2024)
Zachary Grannan, Alexander J. Summers
Resource Specifications for Resource-Manipulating Programs. CoRR (2023)
Zachary Grannan, Niki Vazou, Eva Darulova, Alexander J. Summers
REST: Integrating Term Rewriting with Program Verification. ECOOP (2022)
Zachary Grannan, Niki Vazou, Eva Darulova, Alexander J. Summers
REST: Integrating Term Rewriting with Program Verification (Artifact). Dagstuhl Artifacts Ser. 8 (2) (2022)
Thibault Dardinier, Gaurav Parthasarathy, Noé Weeks, Peter Müller, Alexander J. Summers
Sound Automation of Magic Wands. CAV (2) (2022)
Thibault Dardinier, Peter Müller, Alexander J. Summers
Fractional resources in unbounded separation logic. Proc. ACM Program. Lang. 6 (OOPSLA2) (2022)
Zachary Grannan, Niki Vazou, Eva Darulova, Alexander J. Summers
REST: Integrating Term Rewriting with Program Verification (Extended Version). CoRR (2022)
Vytautas Astrauskas, Aurel Bílý, Jonás Fiala, Zachary Grannan, Christoph Matheja, Peter Müller, Federico Poli, Alexander J. Summers
The Prusti Project: Formal Verification for Rust. NFM (2022)
Thibault Dardinier, Gaurav Parthasarathy, Noé Weeks, Alexander J. Summers, Peter Müller
Sound Automation of Magic Wands (extended version). CoRR (2022)
Alexander J. Summers, Houshang Yin, Ralf D. Fischer, Barton C. Prorok, Xiaoyuan Lou, Q. Peter He
. ACC (2022)
Aurel Bílý, Jonas Hansen, Peter Müller, Alexander J. Summers
Compositional Reasoning for Side-effectful Iterators and Iterator Adapters. CoRR (2022)
Christian Bräm, Marco Eilers, Peter Müller, Robin Sierra, Alexander J. Summers
Rich specifications for Ethereum smart contract verification. Proc. ACM Program. Lang. 5 (OOPSLA) (2021)
Fabian Wolff, Aurel Bílý, Christoph Matheja, Peter Müller, Alexander J. Summers
Modular specification and verification of closures in Rust. Proc. ACM Program. Lang. 5 (OOPSLA) (2021)
Christian Bräm, Marco Eilers, Peter Müller, Robin Sierra, Alexander J. Summers
Modular Verification of Collaborating Smart Contracts. CoRR (2021)
Gaurav Parthasarathy, Peter Müller, Alexander J. Summers
Formally Validating a Practical Verification Condition Generator. CAV (2) (2021)
Elisa L. A. Baniassad, Alexander J. Summers
Reframing the Liskov substitution principle through the lens of testing. SPLASH-E (2021)
Gaurav Parthasarathy, Peter Müller, Alexander J. Summers
Formally Validating a Practical Verification Condition Generator (extended version). CoRR (2021)
Vytautas Astrauskas, Christoph Matheja, Federico Poli, Peter Müller, Alexander J. Summers
How do programmers use unsafe rust? Proc. ACM Program. Lang. 4 (OOPSLA) (2020)
Siddharth Krishna, Alexander J. Summers, Thomas Wies
Local Reasoning for Global Graph Properties. ESOP (2020)
Alexander J. Summers
Prusti: deductive verification for Rust (keynote). FTfJP@ECOOP (2020)
Alexander J. Summers, Peter Müller
Automating deductive verification for weak-memory programs (extended version). Int. J. Softw. Tools Technol. Transf. 22 (6) (2020)
Vytautas Astrauskas, Peter Müller, Federico Poli, Alexander J. Summers
Leveraging rust types for modular specification and verification. Proc. ACM Program. Lang. 3 (OOPSLA) (2019)
Arshavir Ter-Gabrielyan, Alexander J. Summers, Peter Müller
Modular verification of heap reachability properties in separation logic. Proc. ACM Program. Lang. 3 (OOPSLA) (2019)
Siddharth Krishna, Alexander J. Summers, Thomas Wies
Local Reasoning for Global Graph Properties. CoRR (2019)
Arshavir Ter-Gabrielyan, Alexander J. Summers, Peter Müller
Modular Verification of Heap Reachability Properties in Separation Logic. CoRR (2019)
Nils Becker, Peter Müller, Alexander J. Summers
The Axiom Profiler: Understanding and Debugging SMT Quantifier Instantiations. TACAS (1) (2019)
Jérôme Dohrau, Alexander J. Summers, Caterina Urban, Severin Münger, Peter Müller
Permission Inference for Array Programs. CoRR (2018)
Jérôme Dohrau, Alexander J. Summers, Caterina Urban, Severin Münger, Peter Müller
Permission Inference for Array Programs. CAV (2) (2018)
Alexander J. Summers, Peter Müller
Automating Deductive Verification for Weak-Memory Programs. TACAS (1) (2018)
Alexander J. Summers, Peter Müller
Automating Deductive Verification for Weak-Memory Programs. CoRR (2017)
Peter Müller, Malte Schwerhoff, Alexander J. Summers
Viper: A Verification Infrastructure for Permission-Based Reasoning. VMCAI (2016)
Peter Müller, Malte Schwerhoff, Alexander J. Summers
Automatic Verification of Iterated Separating Conjunctions using Symbolic Execution. CoRR (2016)
Alexander J. Summers, Peter Müller
Actor Services - Modular Verification of Message Passing Programs. ESOP (2016)
Peter Müller, Malte Schwerhoff, Alexander J. Summers
Automatic Verification of Iterated Separating Conjunctions Using Symbolic Execution. CAV (1) (2016)
Alexander J. Summers
Software Verification "Across the Stack" (Invited Talk). ECOOP (2015)
Malte Schwerhoff, Alexander J. Summers
Lightweight Support for Magic Wands in an Automatic Verifier (Artifact). Dagstuhl Artifacts Ser. 1 (1) (2015)
Malte Schwerhoff, Alexander J. Summers
Lightweight Support for Magic Wands in an Automatic Verifier. ECOOP (2015)
John Tang Boyland, Peter Müller, Malte Schwerhoff, Alexander J. Summers
Constraint Semantics for Abstract Read Permissions. FTfJP@ECOOP (2014)
Daniel Jost, Alexander J. Summers
An Automatic Encoding from VeriFast Predicates into Implicit Dynamic Frames. VSTTE (2013)
Stefan Heule, Ioannis T. Kassios, Peter Müller, Alexander J. Summers
Verification Condition Generation for Permission Logics with Abstract Predicates and Abstraction Functions. ECOOP (2013)
Stefan Heule, K. Rustan M. Leino, Peter Müller, Alexander J. Summers
Abstract Read Permissions: Fractional Permissions without the Fractions. VMCAI (2013)
Alexander J. Summers, Sophia Drossopoulou
A Formal Semantics for Isorecursive and Equirecursive State Abstractions. ECOOP (2013)
Matthew J. Parkinson, Alexander J. Summers
The Relationship Between Separation Logic and Implicit Dynamic Frames Log. Methods Comput. Sci. 8 (3) (2012)
Alexander J. Summers, Peter Müller
Freedom before commitment: a lightweight type system for object initialisation. OOPSLA (2011)
Matthew J. Parkinson, Alexander J. Summers
The Relationship between Separation Logic and Implicit Dynamic Frames. ESOP (2011)
Stefan Heule, K. Rustan M. Leino, Peter Müller, Alexander J. Summers
Fractional permissions without the fractions. FTfJP@ECOOP (2011)
Alexander J. Summers
Soundness and principal contexts for a shallow polymorphic type system based on classical logic. Log. J. IGPL 19 (6) (2011)
Alexander J. Summers, Nicholas Cameron, Mariangiola Dezani-Ciancaglini, Sophia Drossopoulou
Towards a semantic model for Java wildcards. FTfJP@ECOOP (2010)
Alexander J. Summers, Sophia Drossopoulou
Considerate Reasoning and the Composite Design Pattern. VMCAI (2010)
Alexander J. Summers, Sophia Drossopoulou, Peter Müller
Universe-Type-Based Verification Techniques for Mutable Static Fields and Methods. J. Object Technol. 8 (4) (2009)
Alexander J. Summers
Modelling Java requires state. FTfJP@ECOOP (2009)
Sophia Drossopoulou, Adrian Francalanza, Peter Müller, Alexander J. Summers
A Unified Framework for Verification Techniques for Object Invariants. Types, Logics and Semantics for State (2008)
Sophia Drossopoulou, Adrian Francalanza, Peter Müller, Alexander J. Summers
A Unified Framework for Verification Techniques for Object Invariants. ECOOP (2008)
Dave Cunningham, Werner Dietl, Sophia Drossopoulou, Adrian Francalanza, Peter Müller, Alexander J. Summers
Universe Types for Topology and Encapsulation. FMCO (2007)
Jayshan Raghunandan, Alexander J. Summers
On the Computational Representation of Classical Logical Connectives. Electron. Notes Theor. Comput. Sci. 171 (3) (2007)
Krysia Broda, Jiefei Ma, Gabrielle Sinnadurai, Alexander J. Summers
Pandora: A Reasoning Toolbox using Natural Deduction Style. Log. J. IGPL 15 (4) (2007)
Alexander J. Summers, Steffen van Bakel
Approaches to Polymorphism in Classical Sequent Calculus. ESOP (2006)

Alexander J. Summers.css-eqlu8i{font-size:small;padding-left:4px;}

Publication Activity (10 Years)

Top Topics

Top Venues

Alexander J. Summers