Alexander J. Summers

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