You’ll find my papers listed below - if you notice any data (e.g. pdfs) is missing or incorrect, feel free to let me know. You can find my Google Scholar profile here.

Conference and Journal Papers

  1. Zachary Grannan and Alexander J. Summers. Resource Specifications for Resource-Manipulating Programs (draft). 2023. PDF 
    @misc{GrannanSummers23,
  author = {Grannan, Zachary and Summers, Alexander J.},
  title = {Resource Specifications for Resource-Manipulating Programs (draft)},
  year = {2023},
  eprint = {2304.12530},
  archiveprefix = {arXiv}
}
  2. T. Dardinier, P. Müller, and A. J. Summers. Fractional Resources in Unbounded Separation Logic. Object-Oriented Programming Systems, Languages, and Applications (OOPSLA) 6. ACM SIGPLAN Distinguished Paper Award. 2022. PDF 
    @article{DardinierMuellerSummers22,
  author = {Dardinier, T. and M\"{u}ller, P. and Summers, A. J.},
  title = {Fractional Resources in Unbounded Separation Logic},
  booktitle = {Object-Oriented Programming Systems, Languages, and Applications (OOPSLA)},
  year = {2022},
  issue_date = {October 2022},
  publisher = {Association for Computing Machinery},
  address = {New York, NY, USA},
  volume = {6},
  url = {https://doi.org/10.1145/3563326},
  doi = {10.1145/3563326},
  journal = {Proc. ACM Program. Lang.},
  month = oct,
  articleno = {163},
  numpages = {27},
  urltext = {[Publisher]},
  note = {ACM SIGPLAN Distinguished Paper Award}
}
  3. A. Bílý, J. Hansen, P. Müller, and A. J. Summers. Compositional Reasoning for Side-effectful Iterators and Iterator Adapters. arXiv.2022. PDF 
    @techreport{BilyHansenMuellerSummers22,
  author = {B\'il\'y, A. and Hansen, J. and M\"uller, P. and Summers, A. J.},
  title = {Compositional Reasoning for Side-effectful Iterators and Iterator Adapters},
  institution = {arXiv},
  year = {2022},
  number = {2210.09857},
  url = {https://arxiv.org/abs/2210.09857},
  urltext = {[arXiv]}
}
  4. V. Astrauskas, A. Bílý, J. Fiala, Z. Grannan, C. Matheja, P. Müller, F. Poli, and A. J. Summers. The Prusti Project: Formal Verification for Rust (invited). NASA Formal Methods (14th International Symposium), Springer, 88–108. 2022. PDF 
    @inproceedings{AstrauskasBilyFialaGrannanMathejaMuellerPoliSummers22,
  author = {Astrauskas, V. and B\'il\'y, A. and Fiala, J. and Grannan, Z. and Matheja, C. and M\"uller, P. and Poli, F. and Summers, A. J.},
  title = {The Prusti Project: Formal Verification for Rust (invited)},
  booktitle = {NASA Formal Methods (14th International Symposium)},
  pages = {88--108},
  year = {2022},
  publisher = {Springer},
  url = {https://link.springer.com/chapter/10.1007/978-3-031-06773-0_5},
  urltext = {[Publisher]}
}
  5. T. Dardinier, G. Parthasarathy, N. Weeks, A. J. Summers, and P. Müller. Sound Automation of Magic Wands. Computer Aided Verification (CAV), Springer International Publishing, 131–151. 2022. 
    @inproceedings{DardinierParthasarathyWeeksSummersMueller22,
  author = {Dardinier, T. and Parthasarathy, G. and Weeks, N. and Summers, A. J. and M\"uller, P.},
  editor = {Shoham, Sharon and Vizel, Yakir},
  title = {Sound Automation of Magic Wands},
  booktitle = {Computer Aided Verification (CAV)},
  year = {2022},
  publisher = {Springer International Publishing},
  address = {Cham},
  pages = {131--151},
  isbn = {979-3-031-13188-2},
  url = {https://link.springer.com/chapter/10.1007/978-3-031-13188-2_7},
  urltext = {[Publisher]}
}
  6. T. Dardinier, G. Parthasarathy, N. Weeks, A. J. Summers, and P. Müller. Sound Automation of Magic Wands (extended version). arXiv.2022. PDF 
    @techreport{DardinierParthasarathyWeeksSummersMuellerArxiv22,
  author = {Dardinier, T. and Parthasarathy, G. and Weeks, N. and Summers, A. J. and M\"uller, P.},
  title = {Sound Automation of Magic Wands (extended version)},
  institution = {arXiv},
  year = {2022},
  number = {2205.11325},
  url = {https://arxiv.org/abs/2205.11325},
  urltext = {[arXiv]}
}
  7. Zachary Grannan, Niki Vazou, Eva Darulova, and Alexander J. Summers. REST : Integrating Term Rewriting with Program Verification. 36th European Conference on Object-Oriented Programming (ECOOP 2022). 2022. PDF 
    @misc{GrannanDarulovaSummersVazou21,
  author = {Grannan, Zachary and Vazou, Niki and Darulova, Eva and Summers, Alexander J.},
  booktitle = {36th European Conference on Object-Oriented Programming (ECOOP 2022)},
  institution = {Uppsala University, Computing Science},
  publisher = {Schloss Dagstuhl - Leibniz-Zentrum für Informatik},
  title = {REST : Integrating Term Rewriting with Program Verification},
  series = {Leibniz International Proceedings in Informatics (LIPIcs)},
  number = {222},
  doi = {10.4230/LIPIcs.ECOOP.2022.13},
  keywords = {term rewriting, program verification, theorem proving},
  isbn = {978-3-95977-225-9},
  year = {2022}
}
  8. F. Wolff, A. Bílý, C. Matheja, P. Müller, and A. J. Summers. Modular Specification and Verification of Closures in Rust. Object-Oriented Programming Systems, Languages, and Applications (OOPSLA), ACM. 2021. PDF 
    @inproceedings{WolffBilyMathejaMuellerSummers21,
  author = {Wolff, F. and B\'il\'y, A. and Matheja, C. and M\"uller, P. and Summers, A. J.},
  title = {Modular Specification and Verification of Closures in Rust},
  booktitle = {Object-Oriented Programming Systems, Languages, and Applications (OOPSLA)},
  journal = {Proc. ACM Program. Lang.},
  year = {2021},
  issue_date = {October 2021},
  publisher = {ACM},
  address = {New York, NY, USA},
  volume = {5},
  number = {OOPSLA},
  doi = {10.1145/3485522},
  month = oct,
  articleno = {145},
  numpages = {29}
}
  9. C. Bräm, M. Eilers, P. Müller, R. Sierra, and A. J. Summers. Rich Specifications for Ethereum Smart Contract Verification . Object-Oriented Programming Systems, Languages, and Applications (OOPSLA), ACM. 2021. PDF 
    @inproceedings{BraemEilersMuellerSierraSummers21,
  author = {Br\"am, C. and Eilers, M. and M\"uller, P. and Sierra, R. and Summers, A. J.},
  title = {Rich Specifications for Ethereum Smart Contract Verification },
  booktitle = {Object-Oriented Programming Systems, Languages, and Applications (OOPSLA)},
  journal = {Proc. ACM Program. Lang.},
  year = {2021},
  issue_date = {October 2021},
  publisher = {ACM},
  address = {New York, NY, USA},
  volume = {5},
  number = {OOPSLA},
  doi = {10.1145/3485523},
  articleno = {146},
  numpages = {30}
}
  10. G. Parthasarathy, P. Müller, and A. J. Summers. Formally Validating a Practical Verification Condition Generator. Computer Aided Verification (CAV), Springer International Publishing, 704–727. 2021. PDF 
    @inproceedings{ParthasarathyMuellerSummers21,
  author = {Parthasarathy, G. and M\"uller, P. and Summers, A. J.},
  title = {Formally Validating a Practical Verification Condition Generator},
  booktitle = {Computer Aided Verification (CAV)},
  editor = {Silva, Alexandra and Leino, K. Rustan M.},
  publisher = {Springer International Publishing},
  series = {LNCS},
  volume = {12760},
  pages = {704--727},
  year = {2021}
}
  11. Vytautas Astrauskas, Christoph Matheja, Federico Poli, Peter Müller, and Alexander J. Summers. How Do Programmers Use Unsafe Rust? Object-Oriented Programming Systems, Languages, and Applications (OOPSLA) 2020. 2020. PDF 
    @article{AstrauskasMathejaPoliMuellerSummers20,
  author = {Astrauskas, Vytautas and Matheja, Christoph and Poli, Federico and M\"{u}ller, Peter and Summers, Alexander J.},
  title = {How Do Programmers Use Unsafe Rust?},
  issue_date = {November 2020},
  publisher = {Association for Computing Machinery},
  address = {New York, NY, USA},
  url = {https://doi.org/10.1145/3428204},
  doi = {10.1145/3428204},
  %abstract = {Rust’s ownership type system enforces a strict discipline on how memory locations are accessed and shared. This discipline allows the compiler to statically prevent memory errors, data races, inadvertent side effects through aliasing, and other errors that frequently occur in conventional imperative programs. However, the restrictions imposed by Rust’s type system make it difficult or impossible to implement certain designs, such as data structures that require aliasing (e.g. doubly-linked lists and shared caches). To work around this limitation, Rust allows code blocks to be declared as unsafe and thereby exempted from certain restrictions of the type system, for instance, to manipulate C-style raw pointers. Ensuring the safety of unsafe code is the responsibility of the programmer. However, an important assumption of the Rust language, which we dub the Rust hypothesis, is that programmers use Rust by following three main principles: use unsafe code sparingly, make it easy to review, and hide it behind a safe abstraction such that client code can be written in safe Rust. Understanding how Rust programmers use unsafe code and, in particular, whether the Rust hypothesis holds is essential for Rust developers and testers, language and library designers, as well as tool developers. This paper studies empirically how unsafe code is used in practice by analysing a large corpus of Rust projects to assess the validity of the Rust hypothesis and to classify the purpose of unsafe code. We identify queries that can be answered by automatically inspecting the program’s source code, its intermediate representation MIR, as well as type information provided by the Rust compiler; we complement the results by manual code inspection. Our study supports the Rust hypothesis partially: While most unsafe code is simple and well-encapsulated, unsafe features are used extensively, especially for interoperability with other languages.},
  journal = {Object-Oriented Programming Systems, Languages, and Applications (OOPSLA) 2020},
  year = {2020},
  month = nov,
  articleno = {136},
  numpages = {27},
  keywords = {Rust, unsafe code, empirical study, Rust hypothesis}
}
  12. Siddharth Krishna, Alexander J. Summers, and Thomas Wies. Local Reasoning for Global Graph Properties. European Symposium on Programming (ESOP) 2020, Springer International Publishing, 308–335. 2020. PDF 
    @inproceedings{KrishnaSummersWies20,
  author = {Krishna, Siddharth and Summers, Alexander J. and Wies, Thomas},
  title = {Local Reasoning for Global Graph Properties},
  booktitle = {European Symposium on Programming (ESOP) 2020},
  year = {2020},
  publisher = {Springer International Publishing},
  address = {Cham},
  pages = {308--335},
  isbn = {978-3-030-44914-8}
}
  13. A. J. Summers and P. Müller. Automating Deductive Verification for Weak-Memory Programs (extended version). International Journal on Software Tools for Technology Transfer. 2020. PDF 
    @article{SummersMueller20,
  author = {Summers, A. J. and M\"uller, P.},
  title = {Automating Deductive Verification for Weak-Memory Programs (extended version)},
  journal = {International Journal on Software Tools for Technology Transfer},
  year = {2020},
  month = mar,
  doi = {10.1007/s10009-020-00559-y}
}
  14. V. Astrauskas, P. Müller, F. Poli, and A. J. Summers. Leveraging Rust Types for Modular Specification and Verification. Object-Oriented Programming Systems, Languages, and Applications (OOPSLA) 2019, ACM, 147:1–147:30. 2019. PDF 
    @inproceedings{AstrauskasMuellerPoliSummers19,
  title = {Leveraging {R}ust Types for Modular Specification and Verification},
  author = {Astrauskas, V. and M\"uller, P. and Poli, F. and Summers, A. J.},
  booktitle = {Object-Oriented Programming Systems, Languages, and Applications (OOPSLA) 2019},
  year = {2019},
  pages = {147:1--147:30},
  url = {http://doi.acm.org/10.1145/3360573},
  urltext = {[Publisher]},
  doi = {10.1145/3360573},
  publisher = {ACM}
}
  15. A. Ter-Gabrielyan, A. J. Summers, and P. Müller. Modular Verification of Heap Reachability Properties in Separation Logic. Object-Oriented Programming Systems, Languages, and Applications (OOPSLA) 2019: 121:1–121:28. 2019. PDF 
    @article{TerGabrielyanSummersMueller19,
  author = {Ter-Gabrielyan, A. and Summers, A. J. and M\"uller, P.},
  title = {Modular Verification of Heap Reachability Properties in Separation Logic},
  booktitle = {Object-Oriented Programming Systems, Languages, and Applications (OOPSLA) 2019},
  journal = {Proc. ACM Program. Lang.},
  year = {2019},
  pages = {121:1--121:28},
  url = {http://doi.acm.org/10.1145/3360547},
  urltext = {[Publisher]},
  doi = {10.1145/3360547},
  publisher = {ACM}
}
  16. N. Becker, P. Müller, and A. J. Summers. The Axiom Profiler: Understanding and Debugging SMT Quantifier Instantiations. Tools and Algorithms for the Construction and Analysis of Systems (TACAS) 2019, Springer-Verlag, 99–116. 2019. PDF 
    @inproceedings{BeckerMuellerSummers19,
  author = {Becker, N. and M\"uller, P. and Summers, A. J.},
  title = {The Axiom Profiler: Understanding and Debugging SMT Quantifier Instantiations},
  booktitle = {Tools and Algorithms for the Construction and Analysis of Systems (TACAS) 2019},
  year = {2019},
  series = {LNCS},
  pages = {99--116},
  publisher = {Springer-Verlag}
}
  17. J. Dohrau, A. J. Summers, C. Urban, S. Münger, and P. Müller. Permission Inference for Array Programs (extended version). Computer Aided Verification (CAV), Springer-Verlag, 55–74. 2018. PDF 
    @inproceedings{DohrauSummersUrbanMuengerMueller18,
  author = {Dohrau, J. and Summers, A. J. and Urban, C. and M\"unger, S. and M\"uller, P.},
  title = {Permission Inference for Array Programs (extended version)},
  booktitle = {Computer Aided Verification (CAV)},
  editor = {Chockler, Hana and Weissenbacher, Georg},
  year = {2018},
  series = {LNCS},
  volume = {10982},
  publisher = {Springer-Verlag},
  pages = {55--74},
  doi = {10.1007/978-3-319-96142-2_2},
  url = {https://link.springer.com/chapter/10.1007/978-3-319-96142-2_7},
  urltext = {[Publisher]}
}
  18. A. J. Summers and P. Müller. Automating Deductive Verification for Weak-Memory Programs. Tools and Algorithms for the Construction and Analysis of Systems (TACAS), Springer-Verlag, 190–209. Nominated for Best Paper Award. 2018. PDF 
    @inproceedings{SummersMueller18,
  author = {Summers, A. J. and M\"uller, P.},
  title = {Automating Deductive Verification for Weak-Memory Programs},
  booktitle = {Tools and Algorithms for the Construction and Analysis of Systems (TACAS)},
  year = {2018},
  series = {LNCS},
  publisher = {Springer-Verlag},
  pages = {190--209},
  url = {https://doi.org/10.1007/978-3-319-89960-2_11},
  note = {Nominated for Best Paper Award}
}
  19. P. Müller, M. Schwerhoff, and A. J. Summers. Automatic Verification of Iterated Separating Conjunctions using Symbolic Execution. Computer Aided Verification (CAV), Springer-Verlag, 405–425. 2016. PDF 
    @inproceedings{MuellerSchwerhoffSummers16b,
  author = {M\"uller, P. and Schwerhoff, M. and Summers, A. J.},
  title = {Automatic Verification of Iterated Separating Conjunctions using Symbolic Execution},
  booktitle = {Computer Aided Verification (CAV)},
  editor = {Chaudhuri, S. and Farzan, A.},
  volume = {9779},
  pages = {405--425},
  year = {2016},
  series = {LNCS},
  publisher = {Springer-Verlag},
  url = {http://link.springer.com/chapter/10.1007/978-3-319-41528-4_22},
  urltext = {[Publisher]}
}
  20. A. J. Summers and P. Müller. Actor Services: Modular Verification of Message Passing Programs. European Symposium on Programming (ESOP), Springer Berlin Heidelberg, 699–726. 2016. PDF 
    @inproceedings{SummersMueller16,
  author = {Summers, A. J. and M{\"u}ller, P.},
  title = {Actor Services: Modular Verification of Message Passing Programs},
  booktitle = {European Symposium on Programming (ESOP)},
  editor = {Thiemann, P.},
  year = {2016},
  series = {LNCS},
  publisher = {Springer Berlin Heidelberg},
  pages = {699--726},
  isbn = {978-3-662-49498-1},
  doi = {10.1007/978-3-662-49498-1_27},
  url = {http://dx.doi.org/10.1007/978-3-662-49498-1_27},
  urltext = {[Publisher]}
}
  21. P. Müller, M. Schwerhoff, and A. J. Summers. Viper: A Verification Infrastructure for Permission-Based Reasoning. Verification, Model Checking, and Abstract Interpretation (VMCAI), Springer-Verlag, 41–62. 2016. PDF 
    @inproceedings{MuellerSchwerhoffSummers16,
  author = {M{\"u}ller, P. and Schwerhoff, M. and Summers, A. J.},
  title = {Viper: A Verification Infrastructure for Permission-Based Reasoning},
  booktitle = {Verification, Model Checking, and Abstract Interpretation (VMCAI)},
  editor = {Jobstmann, B. and Leino, K. R. M.},
  year = {2016},
  publisher = {Springer-Verlag},
  series = {LNCS},
  pages = {41-62},
  volume = {9583},
  url = {https://doi.org/10.1007/978-3-662-49122-5_2}
}
  22. M. Schwerhoff and A. J. Summers. Lightweight Support for Magic Wands in an Automatic Verifier. European Conference on Object-Oriented Programming (ECOOP), Schloss Dagstuhl, 614–638. 2015. PDF 
    @inproceedings{SchwerhoffSummers15,
  author = {Schwerhoff, M. and Summers, A. J.},
  title = {{Lightweight Support for Magic Wands in an Automatic Verifier}},
  booktitle = {European Conference on Object-Oriented Programming (ECOOP)},
  pages = {614--638},
  series = {LIPIcs},
  year = {2015},
  volume = {37},
  editor = {Boyland, J. T.},
  publisher = {Schloss Dagstuhl},
  url = {https://doi.org/10.4230/LIPIcs.ECOOP.2015.614},
  urltext = {[Publisher]}
}
  23. D. Jost and A. J. Summers. An automatic encoding from VeriFast Predicates into Implicit Dynamic Frames. Verified Software: Theories, Tools and Experiments (VSTTE), Springer, 202–221. 2013. PDF 
    @inproceedings{JostSummers13,
  author = {Jost, D. and Summers, A. J.},
  title = {An automatic encoding from VeriFast Predicates into Implicit Dynamic Frames},
  booktitle = {Verified Software: Theories, Tools and Experiments (VSTTE)},
  year = {2013},
  volume = {8164},
  series = {Lecture Notes in Computer Science},
  editor = {Cohen, E. and Rybalchenko, A.},
  publisher = {Springer},
  pages = {202-221},
  url = {https://doi.org/10.1007/978-3-642-54108-7_11},
  urltext = {[Publisher]}
}
  24. S. Heule, I. T. Kassios, P. Müller, and A. J. Summers. Verification Condition Generation for Permission Logics with Abstract Predicates and Abstraction Functions. European Conference on Object-Oriented Programming (ECOOP), Springer, 451–476. 2013. PDF 
    @inproceedings{HeuleKassiosMuellerSummers13,
  author = {Heule, S. and Kassios, I. T. and M{\"u}ller, P. and Summers, A. J.},
  title = {Verification Condition Generation for Permission Logics with Abstract Predicates and Abstraction Functions},
  booktitle = {European Conference on Object-Oriented Programming (ECOOP)},
  volume = {7920},
  series = {Lecture Notes in Computer Science},
  editor = {Castagna, Giuseppe},
  year = {2013},
  publisher = {Springer},
  pages = {451-476},
  url = {https://doi.org/10.1007/978-3-642-39038-8_19},
  urltext = {[Publisher]}
}
  25. A. J. Summers and S. Drossopoulou. A Formal Semantics for Isorecursive and Equirecursive State Abstractions. European Conference on Object-Oriented Programming (ECOOP), Springer, 129–153. 2013. PDF 
    @inproceedings{SummersDrossopoulou13,
  author = {Summers, A. J. and Drossopoulou, S.},
  title = {A Formal Semantics for Isorecursive
  and Equirecursive State Abstractions},
  booktitle = {European Conference on Object-Oriented Programming (ECOOP)},
  volume = {7920},
  series = {Lecture Notes in Computer Science},
  editor = {Castagna, Giuseppe},
  year = {2013},
  pages = {129-153},
  publisher = {Springer},
  url = {https://doi.org/10.1007/978-3-642-39038-8_6},
  urltext = {[Publisher]}
}
  26. S. Heule, K. R. M. Leino, P. Müller, and A. J. Summers. Abstract Read Permissions: Fractional Permissions without the Fractions. Verification, Model Checking, and Abstract Interpretation (VMCAI), 315–334. 2013. PDF 
    @inproceedings{HeuleLeinoMuellerSummers13,
  author = {Heule, S. and Leino, K. R. M. and M\"uller, P. and Summers, A. J.},
  title = {Abstract Read Permissions: Fractional Permissions without the Fractions},
  booktitle = {Verification, Model Checking, and Abstract Interpretation (VMCAI)},
  year = {2013},
  series = {Lecture Notes in Computer Science},
  pages = {315--334},
  volume = {7737},
  url = {https://doi.org/10.1007/978-3-642-35873-9_20},
  urltext = {[Publisher]}
}
  27. M. J. Parkinson and A. J. Summers. The Relationship Between Separation Logic and Implicit Dynamic Frames. Logical Methods in Computer Science 8, 3:01: 1–54. 2012. PDF 
    @article{ParkinsonSummers12,
  author = {Parkinson, M. J. and Summers, A. J.},
  title = {The Relationship Between Separation Logic and Implicit Dynamic Frames},
  journal = {Logical Methods in Computer Science},
  year = {2012},
  volume = {8},
  number = {3:01},
  pages = {1--54},
  url = {https://doi.org/10.1007/978-3-642-35182-2_8},
  urltext = {[Publisher]}
}
  28. A. J. Summers and P. Müller. Freedom Before Commitment - A Lightweight Type System for Object Initialisation. Object-Oriented Programming, Systems, Languages and Applications (OOPSLA), ACM, 1013–1032. 2011. PDF 
    @inproceedings{SummersMueller11,
  author = {Summers, A. J. and M\"uller, P.},
  title = {Freedom Before Commitment - A Lightweight Type System for Object Initialisation},
  booktitle = {Object-Oriented Programming, Systems, Languages and Applications (OOPSLA)},
  year = {2011},
  pages = {1013--1032},
  publisher = {ACM},
  url = {http://doi.acm.org/10.1145/2048066.2048142},
  urltext = {[Publisher]}
}
  29. M. J. Parkinson and A. J. Summers. The Relationship Between Separation Logic and Implicit Dynamic Frames. European Symposium on Programming (ESOP), Springer-Verlag, 439–458. 2011. PDF 
    @inproceedings{ParkinsonSummers11,
  author = {Parkinson, M. J. and Summers, A. J.},
  title = {The Relationship Between Separation Logic and Implicit Dynamic Frames},
  booktitle = {European Symposium on Programming (ESOP)},
  editor = {Barthe, Gilles},
  year = {2011},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer-Verlag},
  volume = {6602},
  pages = {439-458},
  url = {https://doi.org/10.1007/978-3-642-19718-5_23},
  urltext = {[Publisher]}
}
  30. A. J. Summers. Soundness and Principal Contexts for a Shallow Polymorphic Type System based on Classical Logic. Logic Journal of IGPL. 2010. PDF 
    @article{Summers10,
  author = {Summers, A. J.},
  title = {Soundness and Principal Contexts for a Shallow Polymorphic Type System based on Classical Logic},
  doi = {10.1093/jigpal/jzq013},
  eprint = {http://jigpal.oxfordjournals.org/content/early/2010/06/29/jigpal.jzq013.full.pdf+html},
  journal = {Logic Journal of IGPL},
  year = {2010},
  url = {http://jigpal.oxfordjournals.org/content/early/2010/06/29/jigpal.jzq013.abstract},
  urltext = {[Publisher]}
}
  31. A. J. Summers and S. Drossopoulou. Considerate Reasoning and the Composite Design Pattern. Verification, Model Checking, and Abstract Interpretation (VMCAI), 328–344. 2010. PDF 
    @inproceedings{SummersDrossopoulou10,
  author = {Summers, A. J. and Drossopoulou, S.},
  title = {Considerate Reasoning and the Composite Design Pattern},
  booktitle = {Verification, Model Checking, and Abstract Interpretation (VMCAI)},
  year = {2010},
  series = {Lecture Notes in Computer Science},
  editor = {Barthe, G. and Hermenegildo, M. V.},
  volume = {5944},
  pages = {328-344},
  url = {https://doi.org/10.1007/978-3-642-11319-2_24},
  urltext = {[Publisher]}
}
  32. Alexander J. Summers. Curry-Howard Term Calculi for Gentzen-Style Classical Logics. Ph.D. thesis examined November 2008; awarded Summer 2009. 2009. PDF 
    @phdthesis{SummersThesis09,
  author = {Summers, Alexander J.},
  title = {Curry-Howard Term Calculi for Gentzen-Style Classical Logics},
  school = {Imperial College London},
  year = {2009},
  note = {Ph.D. thesis examined November 2008; awarded Summer 2009}
}
  33. A. J. Summers, S. Drossopoulou, and P. Müller. Universe-Type-Based Verification Techniques for Mutable Static Fields and Methods. Journal of Object Technology (JOT) 8, 4. 2009. PDF 
    @article{SummersDrossopoulouMueller09,
  author = {Summers, A. J. and Drossopoulou, S. and M\"{u}ller, P.},
  title = {Universe-Type-Based Verification Techniques for Mutable Static Fields and Methods},
  journal = {Journal of Object Technology (JOT)},
  month = jun,
  volume = {8},
  number = {4},
  year = {2009},
  url = {https://doi.org/10.5381/jot.2009.8.4.a4},
  urltext = {[Publisher]}
}
  34. D. Cunningham, W. Dietl, S. Drossopoulou, A. Francalanza, P. Müller, and A. J. Summers. Universe Types for Topology and Encapsulation. Formal Methods for Components and Objects (FMCO), Springer-Verlag, 72–112. 2008. PDF 
    @inproceedings{CunninghamDietlDrossopoulouFrancalanzaMuellerSummers08,
  author = {Cunningham, D. and Dietl, W. and Drossopoulou, S. and Francalanza, A. and M\"{u}ller, P. and Summers, A. J.},
  title = {Universe Types for Topology and Encapsulation},
  booktitle = {Formal Methods for Components and Objects (FMCO)},
  year = {2008},
  editor = {de Boer, F. S. and Bonsangue, M. M. and Graf, S. and de Roever, W.-P.},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer-Verlag},
  volume = {5382},
  pages = {72--112},
  url = {https://doi.org/10.1007/978-3-540-87873-5_17},
  urltext = {[Publisher]}
}
  35. S. Drossopoulou, A. Francalanza, P. Müller, and A. J. Summers. A Unified Framework for Verification Techniques for Object Invariants. European Conference on Object-Oriented Programming (ECOOP), Springer-Verlag, 412–437. 2008. PDF 
    @inproceedings{DrossopoulouFrancalanzaMuellerSummers08,
  author = {Drossopoulou, S. and Francalanza, A. and M{\"u}ller, P. and Summers, A. J.},
  title = {A Unified Framework for Verification Techniques for Object Invariants},
  booktitle = {European Conference on Object-Oriented Programming (ECOOP)},
  year = {2008},
  editor = {Vitek, J.},
  pages = {412--437},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer-Verlag},
  volume = {5142},
  url = {https://doi.org/10.1007/978-3-540-70592-5_18},
  urltext = {[Publisher]}
}
  36. Alexander J. Summers and Steffen van Bakel. Approaches to Polymorphism in Classical Sequent Calculus. European Symposium on Programming (ESOP) 2006, Springer Berlin Heidelberg, 84–99. 2006. PDF 
    @inproceedings{SummersvanBakel06,
  author = {Summers, Alexander J. and van Bakel, Steffen},
  editor = {Sestoft, Peter},
  title = {Approaches to Polymorphism in Classical Sequent Calculus},
  booktitle = {European Symposium on Programming (ESOP) 2006},
  year = {2006},
  publisher = {Springer Berlin Heidelberg},
  address = {Berlin, Heidelberg},
  pages = {84--99},
  isbn = {978-3-540-33096-7}
}

Workshop Papers

  1. J. Boyland, P. Müller, M. Schwerhoff, and A. J. Summers. Constraint Semantics for Abstract Read Permissions. Formal Techniques for Java-like Programs (FTfJP), ACM. 2014. PDF 
    @inproceedings{BoylandMuellerSchwerhoffSummers14,
  author = {Boyland, J. and M{\"u}ller, P. and Schwerhoff, M. and Summers, A. J.},
  title = {Constraint Semantics for Abstract Read Permissions},
  booktitle = {Formal Techniques for Java-like Programs (FTfJP)},
  year = {2014},
  publisher = {ACM},
  url = {http://doi.acm.org/10.1145/2635631.2635847},
  urltext = {[Publisher]}
}
  2. S. Heule, K. R. M. Leino, P. Müller, and A. J. Summers. Fractional Permissions Without the Fractions. Formal Techniques for Java-like Programs (FTfJP). 2011. PDF 
    @inproceedings{HeuleLeinoMuellerSummers11,
  author = {Heule, S. and Leino, K. R. M. and M{\"u}ller, P. and Summers, A. J.},
  title = {Fractional Permissions Without the Fractions},
  booktitle = {Formal Techniques for {J}ava-like Programs (FTfJP)},
  year = {2011},
  url = {http://doi.acm.org/10.1145/2076674.2076675},
  urltext = {[Publisher]}
}
  3. Clément Hurlin, François Bobot, and Alexander J. Summers. Size Does Matter: Two Certified Abstractions to Disprove Entailment in Intuitionistic and Classical Separation Logic. International Workshop on Aliasing, Confinement and Ownership in Object-Oriented Programming. 2009. PDF 
    @inproceedings{HurlinBobotSummers09,
  author = {Hurlin, Cl\'{e}ment and Bobot, Fran\c{c}ois and Summers, Alexander J.},
  title = {Size Does Matter: Two Certified Abstractions to Disprove Entailment in Intuitionistic and Classical Separation Logic},
  year = {2009},
  url = {https://doi.org/10.1145/1562154.1562159},
  doi = {10.1145/1562154.1562159},
  booktitle = {International Workshop on Aliasing, Confinement and Ownership in Object-Oriented Programming},
  articleno = {5},
  numpages = {6},
  location = {Genova, Italy},
  series = {IWACO '09}
}
  4. A. J. Summers, S. Drossopoulou, and P. Müller. The Need for Flexible Object Invariants. International Workshop on Aliasing, Confinement and Ownership in object-oriented programming (IWACO). 2009. PDF 
    @inproceedings{SummersDrossopoulouMueller09a,
  author = {Summers, A. J. and Drossopoulou, S. and M\"{u}ller, P.},
  title = {The Need for Flexible Object Invariants},
  booktitle = {International Workshop on Aliasing, Confinement and Ownership in object-oriented programming (IWACO)},
  year = {2009}
}
  5. Alexander J. Summers. Modelling Java Requires State. Proceedings of the 11th International Workshop on Formal Techniques for Java-like Programs. 2009. PDF 
    @inproceedings{Summers09,
  author = {Summers, Alexander J.},
  title = {Modelling Java Requires State},
  year = {2009},
  url = {https://doi.org/10.1145/1557898.1557908},
  doi = {10.1145/1557898.1557908},
  booktitle = {Proceedings of the 11th International Workshop on Formal Techniques for Java-like Programs},
  articleno = {10},
  numpages = {3},
  location = {Genova, Italy},
  series = {FTfJP '09}
}
  6. A. J. Summers, S. Drossopoulou, and P. Müller. A Universe-Type-Based Verification Technique for Mutable Static Fields and Methods. Formal Techniques for Java-like Programs. 2008. PDF 
    @inproceedings{SummersDrossopoulouMueller08,
  author = {Summers, A. J. and Drossopoulou, S. and M{\"u}ller, P.},
  title = {A Universe-Type-Based Verification Technique for Mutable Static Fields and Methods},
  booktitle = {Formal Techniques for {J}ava-like Programs},
  year = {2008}
}
  7. Jayshan Raghunandan and Alexander Summers. On the Computational Representation of Classical Logical Connectives. Electr. Notes Theor. Comput. Sci. 171: 85–109. 2007. PDF 
    @article{RaghunandanSummers07,
  author = {Raghunandan, Jayshan and Summers, Alexander},
  year = {2007},
  month = jun,
  pages = {85-109},
  title = {On the Computational Representation of Classical Logical Connectives},
  volume = {171},
  journal = {Electr. Notes Theor. Comput. Sci.},
  doi = {10.1016/j.entcs.2006.12.039}
}

Teaching Publications

  1. Elisa Baniassad and Alexander J. Summers. Reframing the Liskov Substitution Principle through the Lens of Testing. Proceedings of the 2021 ACM SIGPLAN International Symposium on SPLASH-E, Association for Computing Machinery, 49–58. 2021. PDF 
    @inproceedings{BaniassadSummers21,
  author = {Baniassad, Elisa and Summers, Alexander J.},
  title = {Reframing the Liskov Substitution Principle through the Lens of Testing},
  year = {2021},
  publisher = {Association for Computing Machinery},
  url = {https://doi.org/10.1145/3484272.3484965},
  doi = {10.1145/3484272.3484965},
  booktitle = {Proceedings of the 2021 ACM SIGPLAN International Symposium on SPLASH-E},
  pages = {49–-58},
  numpages = {10},
  location = {Chicago, IL, USA},
  series = {SPLASH-E 2021}
}
  2. Krysia Broda, Jiefei Ma, Gabrielle Sinnadurai, and Alexander J. Summers. Pandora: A Reasoning Toolbox using Natural Deduction Style. Special issue of Logic Journal of the IGPL 2007 on Tools for Teaching Logic 15, 4: 293–304. 2007. PDF 
    @article{BrodaMaSinnaduraiSummers07,
  author = {Broda, Krysia and Ma, Jiefei and Sinnadurai, Gabrielle and Summers, Alexander J.},
  title = {Pandora: A Reasoning Toolbox using Natural Deduction Style},
  year = {2007},
  volume = {15},
  number = {4},
  journal = {Special issue of Logic Journal of the IGPL 2007 on Tools for Teaching Logic},
  pages = {293--304}
}
  3. Krysia Broda, Jiefei Ma, Gabrielle Sinnadurai, and Alexander J. Summers. Pandora - Making Natural Deduction Easy. International Congress on Tools for Teaching Logic (ICTTL), 11–14. 2006. PDF 
    @inproceedings{BrodaMaSinnaduraiSummers06b,
  author = {Broda, Krysia and Ma, Jiefei and Sinnadurai, Gabrielle and Summers, Alexander J.},
  title = {Pandora - Making Natural Deduction Easy},
  year = {2006},
  booktitle = {International Congress on Tools for Teaching Logic (ICTTL)},
  pages = {11--14}
}
  4. Krysia Broda, Jiefei Ma, Gabrielle Sinnadurai, and Alexander J. Summers. Friendly e-tutor for Natural Deduction. Teaching Formal Methods (TFM), BCS-FACS, 1–6. 2006. PDF 
    @inproceedings{BrodaMaSinnaduraiSummers06,
  author = {Broda, Krysia and Ma, Jiefei and Sinnadurai, Gabrielle and Summers, Alexander J.},
  title = {Friendly e-tutor for Natural Deduction},
  year = {2006},
  booktitle = {Teaching Formal Methods (TFM)},
  publisher = {BCS-FACS},
  pages = {1--6}
}

Selected Tech Reports

  1. V. Astrauskas, P. Müller, F. Poli, and A. J. Summers. Leveraging Rust Types for Modular Specification and Verification. ETH Zurich.2019. PDF 
    @techreport{AstrauskasMuellerPoliSummers19,
  author = {Astrauskas, V. and M\"uller, P. and Poli, F. and Summers, A. J.},
  title = {Leveraging {R}ust Types for Modular Specification and Verification},
  institution = {ETH Zurich},
  year = {2019},
  doi = {10.3929/ethz-b-000311092},
  url = {https://doi.org/10.3929/ethz-b-000311092},
  urltext = {[ETH Collection]}
}
  2. J. Dohrau, A. J. Summers, C. Urban, S. Münger, and P. Müller. Permission Inference for Array Programs (extended version). arXiv.2018. PDF 
    @techreport{DohrauSummersUrbanMuengerMueller18,
  author = {Dohrau, J. and Summers, A. J. and Urban, C. and M\"unger, S. and M\"uller, P.},
  title = {Permission Inference for Array Programs (extended version)},
  institution = {arXiv},
  year = {2018},
  number = {1804.04091},
  url = {https://arxiv.org/abs/1804.04091},
  urltext = {[arXiv]}
}
  3. U. Juhasz, I. T. Kassios, P. Müller, M. Novacek, M. Schwerhoff, and A. J. Summers. Viper: A Verification Infrastructure for Permission-Based Reasoning. ETH Zurich.2014. PDF 
    @techreport{JuhaszKassiosMuellerNovacekSchwerhoffSummers14,
  author = {Juhasz, U. and Kassios, I. T. and M{\"u}ller, P. and Novacek, M. and Schwerhoff, M. and Summers, A. J.},
  title = {Viper: A Verification Infrastructure for Permission-Based Reasoning},
  institution = {ETH Zurich},
  year = {2014}
}