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. Grannan, Z., Darulova, E., Summers, A. J., & Vazou, N. (2021). REST: Integrating Term Rewriting with Program Verification (draft paper). PDF
    @misc{Grannan21,
      author = {Grannan, Zachary and Darulova, Eva and Summers, Alexander J. and Vazou, Niki},
      title = {REST: Integrating Term Rewriting with Program Verification (draft paper)},
      year = {2021}
    }
    
  2. Wolff, F., Bílý, A., Matheja, C., Müller, P., & Summers, A. J. (2021). Modular Specification and Verification of Closures in Rust (draft paper). PDF
    @misc{WolffBilyMathejaMuellerSummers21,
      author = {Wolff, Fabian and B\'il\'y, Aurel and Matheja, Christoph and M\"uller, Peter and Summers, Alexander J.},
      title = {Modular Specification and Verification of Closures in Rust (draft paper)},
      year = {2021}
    }
    
  3. Bräm, C., Eilers, M., Müller, P., Sierra, R., & Summers, A. J. (2021). Rich Specifications for Ethereum Smart Contract Verification (draft paper). PDF
    @misc{BraemEilersMuellerSierraSummers21,
      author = {Br\"am, Christian and Eilers, Marco and M\"uller, Peter and Sierra, Robin and Summers, Alexander J.},
      title = {Rich Specifications for Ethereum Smart Contract
      Verification (draft paper)},
      year = {2021}
    }
    
  4. Parthasarathy, G., Müller, P., & Summers, A. J. (2021). Formally Validating a Practical Verification Condition Generator. In (draft); accepted for publication at Computer-Aided Verification (CAV) 2021. PDF
    @misc{ParthasarathyMuellerSummers21,
      author = {Parthasarathy, Gaurav and M\"uller, Peter and Summers, Alexander J.},
      title = {Formally Validating a Practical Verification Condition Generator},
      journal = {(draft); accepted for publication at Computer-Aided Verification (CAV) 2021},
      year = {2021}
    }
    
  5. Astrauskas, V., Matheja, C., Poli, F., Müller, P., & Summers, A. J. (2020). How Do Programmers Use Unsafe Rust? Object-Oriented Programming Systems, Languages, and Applications (OOPSLA) 2020. https://doi.org/10.1145/3428204 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}
    }
    
  6. Krishna, S., Summers, A. J., & Wies, T. (2020). Local Reasoning for Global Graph Properties. European Symposium on Programming (ESOP) 2020, 308–335. 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}
    }
    
  7. Summers, A. J., & Müller, P. (2020). Automating Deductive Verification for Weak-Memory Programs (extended version). International Journal on Software Tools for Technology Transfer. https://doi.org/10.1007/s10009-020-00559-y 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}
    }
    
  8. Astrauskas, V., Müller, P., Poli, F., & Summers, A. J. (2019). Leveraging Rust Types for Modular Specification and Verification. Object-Oriented Programming Systems, Languages, and Applications (OOPSLA) 2019, 147:1–147:30. https://doi.org/10.1145/3360573 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}
    }
    
  9. Ter-Gabrielyan, A., Summers, A. J., & Müller, P. (2019). Modular Verification of Heap Reachability Properties in Separation Logic. Object-Oriented Programming Systems, Languages, and Applications (OOPSLA) 2019, 121:1–121:28. https://doi.org/10.1145/3360547 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}
    }
    
  10. Becker, N., Müller, P., & Summers, A. J. (2019). The Axiom Profiler: Understanding and Debugging SMT Quantifier Instantiations. Tools and Algorithms for the Construction and Analysis of Systems (TACAS) 2019, 99–116. 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}
    }
    
  11. Dohrau, J., Summers, A. J., Urban, C., Münger, S., & Müller, P. (2018). Permission Inference for Array Programs. In H. Chockler & G. Weissenbacher (Eds.), Computer Aided Verification (CAV) (Vol. 10982, pp. 55–74). Springer-Verlag. https://doi.org/10.1007/978-3-319-96142-2_2 PDF
    @inproceedings{Dohrau18,
      author = {Dohrau, J. and Summers, A. J. and Urban, C. and M\"unger, S. and M\"uller, P.},
      title = {Permission Inference for Array Programs},
      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]}
    }
    
  12. Summers, A. J., & Müller, P. (2018). Automating Deductive Verification for Weak-Memory Programs. Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 190–209. https://doi.org/10.1007/978-3-319-89960-2_11 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}
    }
    
  13. Müller, P., Schwerhoff, M., & Summers, A. J. (2016). Automatic Verification of Iterated Separating Conjunctions using Symbolic Execution. In S. Chaudhuri & A. Farzan (Eds.), Computer Aided Verification (CAV) (Vol. 9779, pp. 405–425). Springer-Verlag. http://link.springer.com/chapter/10.1007/978-3-319-41528-4_22 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]}
    }
    
  14. Summers, A. J., & Müller, P. (2016). Actor Services: Modular Verification of Message Passing Programs. In P. Thiemann (Ed.), European Symposium on Programming (ESOP) (pp. 699–726). Springer Berlin Heidelberg. https://doi.org/10.1007/978-3-662-49498-1_27 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]}
    }
    
  15. Müller, P., Schwerhoff, M., & Summers, A. J. (2016). Viper: A Verification Infrastructure for Permission-Based Reasoning. In B. Jobstmann & K. R. M. Leino (Eds.), Verification, Model Checking, and Abstract Interpretation (VMCAI) (Vol. 9583, pp. 41–62). Springer-Verlag. https://doi.org/10.1007/978-3-662-49122-5_2 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}
    }
    
  16. Schwerhoff, M., & Summers, A. J. (2015). Lightweight Support for Magic Wands in an Automatic Verifier. In J. T. Boyland (Ed.), European Conference on Object-Oriented Programming (ECOOP) (Vol. 37, pp. 614–638). Schloss Dagstuhl. https://doi.org/10.4230/LIPIcs.ECOOP.2015.614 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]}
    }
    
  17. Jost, D., & Summers, A. J. (2013). An automatic encoding from VeriFast Predicates into Implicit Dynamic Frames. In E. Cohen & A. Rybalchenko (Eds.), Verified Software: Theories, Tools and Experiments (VSTTE) (Vol. 8164, pp. 202–221). Springer. https://doi.org/10.1007/978-3-642-54108-7_11 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]}
    }
    
  18. Heule, S., Kassios, I. T., Müller, P., & Summers, A. J. (2013). Verification Condition Generation for Permission Logics with Abstract Predicates and Abstraction Functions. In G. Castagna (Ed.), European Conference on Object-Oriented Programming (ECOOP) (Vol. 7920, pp. 451–476). Springer. https://doi.org/10.1007/978-3-642-39038-8_19 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]}
    }
    
  19. Summers, A. J., & Drossopoulou, S. (2013). A Formal Semantics for Isorecursive and Equirecursive State Abstractions. In G. Castagna (Ed.), European Conference on Object-Oriented Programming (ECOOP) (Vol. 7920, pp. 129–153). Springer. https://doi.org/10.1007/978-3-642-39038-8_6 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]}
    }
    
  20. Heule, S., Leino, K. R. M., Müller, P., & Summers, A. J. (2013). Abstract Read Permissions: Fractional Permissions without the Fractions. Verification, Model Checking, and Abstract Interpretation (VMCAI), 7737, 315–334. https://doi.org/10.1007/978-3-642-35873-9_20 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]}
    }
    
  21. Parkinson, M. J., & Summers, A. J. (2012). The Relationship Between Separation Logic and Implicit Dynamic Frames. Logical Methods in Computer Science, 8(3:01), 1–54. https://doi.org/10.1007/978-3-642-35182-2_8 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]}
    }
    
  22. Summers, A. J., & Müller, P. (2011). Freedom Before Commitment - A Lightweight Type System for Object Initialisation. Object-Oriented Programming, Systems, Languages and Applications (OOPSLA), 1013–1032. http://doi.acm.org/10.1145/2048066.2048142 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]}
    }
    
  23. Parkinson, M. J., & Summers, A. J. (2011). The Relationship Between Separation Logic and Implicit Dynamic Frames. In G. Barthe (Ed.), European Symposium on Programming (ESOP) (Vol. 6602, pp. 439–458). Springer-Verlag. https://doi.org/10.1007/978-3-642-19718-5_23 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]}
    }
    
  24. Summers, A. J. (2010). Soundness and Principal Contexts for a Shallow Polymorphic Type System based on Classical Logic. Logic Journal of IGPL. https://doi.org/10.1093/jigpal/jzq013 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]}
    }
    
  25. Summers, A. J., & Drossopoulou, S. (2010). Considerate Reasoning and the Composite Design Pattern. In G. Barthe & M. V. Hermenegildo (Eds.), Verification, Model Checking, and Abstract Interpretation (VMCAI) (Vol. 5944, pp. 328–344). https://doi.org/10.1007/978-3-642-11319-2_24 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]}
    }
    
  26. Summers, A. J., Drossopoulou, S., & Müller, P. (2009). Universe-Type-Based Verification Techniques for Mutable Static Fields and Methods. Journal of Object Technology (JOT), 8(4). https://doi.org/10.5381/jot.2009.8.4.a4 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]}
    }
    
  27. Cunningham, D., Dietl, W., Drossopoulou, S., Francalanza, A., Müller, P., & Summers, A. J. (2008). Universe Types for Topology and Encapsulation. In F. S. de Boer, M. M. Bonsangue, S. Graf, & W.-P. de Roever (Eds.), Formal Methods for Components and Objects (FMCO) (Vol. 5382, pp. 72–112). Springer-Verlag. https://doi.org/10.1007/978-3-540-87873-5_17 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]}
    }
    
  28. Drossopoulou, S., Francalanza, A., Müller, P., & Summers, A. J. (2008). A Unified Framework for Verification Techniques for Object Invariants. In J. Vitek (Ed.), European Conference on Object-Oriented Programming (ECOOP) (Vol. 5142, pp. 412–437). Springer-Verlag. https://doi.org/10.1007/978-3-540-70592-5_18 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]}
    }
    

Workshop Papers

  1. Boyland, J., Müller, P., Schwerhoff, M., & Summers, A. J. (2014). Constraint Semantics for Abstract Read Permissions. Formal Techniques for Java-like Programs (FTfJP). http://doi.acm.org/10.1145/2635631.2635847
    @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. Heule, S., Leino, K. R. M., Müller, P., & Summers, A. J. (2011). Fractional Permissions Without the Fractions. Formal Techniques for Java-like Programs (FTfJP). http://doi.acm.org/10.1145/2076674.2076675
    @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. Summers, A. J., Drossopoulou, S., & Müller, P. (2009). The Need for Flexible Object Invariants. International Workshop on Aliasing, Confinement and Ownership in Object-Oriented Programming (IWACO).
    @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}
    }
    
  4. Summers, A. J., Drossopoulou, S., & Müller, P. (2008). A Universe-Type-Based Verification Technique for Mutable Static Fields and Methods. Formal Techniques for Java-like Programs.
    @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}
    }
    

Selected Tech Reports

  1. Astrauskas, V., Müller, P., Poli, F., & Summers, A. J. (2019). Leveraging Rust Types for Modular Specification and Verification. ETH Zurich. https://doi.org/10.3929/ethz-b-000311092 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. Dohrau, J., Summers, A. J., Urban, C., Münger, S., & Müller, P. (2018). Permission Inference for Array Programs (extended version) (No.1804.04091; Number 1804.04091). arXiv. https://arxiv.org/abs/1804.04091
    @techreport{DohrauArxiv18,
      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. Juhasz, U., Kassios, I. T., Müller, P., Novacek, M., Schwerhoff, M., & Summers, A. J. (2014). Viper: A Verification Infrastructure for Permission-Based Reasoning. ETH Zurich.
    @techreport{JKMNSS14,
      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}
    }
    
  4. Summers, A. J., & Müller, P. (2011). Freedom Before Commitment : Simple Flexible Initialisation for Non-Null Types (No.716; Number 716). ETH Zurich.
    @techreport{SummersMuellerTR11,
      author = {Summers, A. J. and M\"uller, P.},
      title = {Freedom Before Commitment :
      Simple Flexible Initialisation for Non-Null Types},
      institution = {ETH Zurich},
      year = {2011},
      number = {716}
    }