Task 4 Papers

[1] Andrea Cerone, Alexey Gotsman, and Hongseok Yang. Algebraic laws for weak consistency. In CONCUR 2017: Proceedings of 28th International Conference on Concurrency Theory, September 2017. [ bib | DOI | .html | Abstract ]
[2] Thomas Dinsdale-Young, Pedro da Rocha Pinto, Kristoffer Just Andersen, and Lars Birkedal. Caper: Automatic Verification for Fine-grained Concurrency. In Proc. ESOP 2017: 26th European Symposium on Programming, Lecture Notes in Computer Science. Springer, April 2017. [ bib | .pdf | Abstract ]
[3] Shale Xiong, Pedro da Rocha Pinto, Gian Ntzik, and Philippa Gardner. Abstract Specifications for Concurrent Maps. In Proc. ESOP 2017: 26th European Symposium on Programming, Lecture Notes in Computer Science. Springer, April 2017. [ bib | .pdf | Abstract ]
[4] Morten Krogh-Jespersen, Kasper Svendsen, and Lars Birkedal. A relational model of types-and-effects in higher-order concurrent separation logic. In POPL 2017: The 44st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Paris, France, pages 218-231, New York, NY, USA, January 2017. ACM. [ bib | DOI | http | Abstract ]
[5] Gian Ntzik. Reasoning About POSIX File Systems. PhD thesis, Imperial College London, 2017. [ bib | .pdf | Abstract ]
[6] Pedro da Rocha Pinto. Reasoning with Time and Data Abstractions. PhD thesis, Imperial College London, 2017. [ bib | .pdf | Abstract ]
[7] Azalea Raad. Abstraction, Refinement and Concurrent Reasoning. PhD thesis, Imperial College London, 2017. [ bib | .pdf | Abstract ]
[8] José Fragoso Santos, Philippa Gardner, Petar Maksimovic, and Daiva Naudziuniene. Towards logic-based verification of javascript programs. In Leonardo de Moura, editor, CADE 2017: Automated Deduction - CADE 26 - 26th International Conference on Automated Deduction, Gothenburg, Sweden, August 6-11, 2017, Proceedings, volume 10395 of Lecture Notes in Computer Science, pages 8-25. Springer, 2017. [ bib | DOI | .html ]
[9] Victor B. F. Gomes, Martin Kleppmann, Dominic P. Mulligan, and Alastair R. Beresford. Verifying strong eventual consistency in distributed systems. In OOPSLA 2017: Proceedings of the ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA), 2017. To appear. [ bib ]
[10] Cristina Matache, Victor B. F. Gomes, and Dominic P. Mulligan. Programming and proving with classical types. In APLAS 2017: Proceedings of the 15th Asian Symposium on Programming Languages and Systems, 2017. To appear. [ bib ]
[11] Lars Birkedal, Thomas Dinsdale-Young, Guilhem Jaber, Kasper Svendsen, and Nikos Tzevelekos. Trace properties from separation logic specifications. CoRR, abs/1702.02972, 2017. [ bib | http | http | Abstract ]
[12] Victor B. F. Gomes and Georg Struth. Modal Kleene algebra applied to program correctness. In John S. Fitzgerald, Stefania Gnesi, and Constance L. Heitmeyer, editors, FM 2016: Formal Methods - 21st International Symposium, Limassol, Lecture Notes in Computer Science, pages 310-325. Springer, November 2016. [ bib | DOI | http | .pdf | Abstract ]
[13] Azalea Raad, Aquinas Hobor, Jules Villard, and Philippa Gardner. Verifying concurrent graph algorithms. In Proc. APLAS 2016: 14th Asian Symposium on Programming Languages and Systems, pages 314-334, November 2016. [ bib | DOI | http | Abstract ]
[14] Azalea Raad, José Fragoso Santos, and Philippa Gardner. DOM: specification and client reasoning. In Proc. APLAS 2016: 14th Asian Symposium on Programming Languages and Systems, pages 401-422, November 2016. [ bib | DOI | http | Abstract ]
[15] Hannes Mehnert and Louis Gesbert. Conex - establishing trust into data repositories. In Proceedings of the ACM OCaml 2016 Workshop, September 2016. [ bib | .pdf | Abstract ]
[16] Enguerrand Decorne, Jeremy Yallop, and David Meršinjak. Ocaml inside: a drop-in replacement for libtls (extended abstract). In Proceedings of the ACM OCaml 2016 Workshop, September 2016. [ bib | .pdf | Abstract ]
[17] Andreas Haas, Thomas A. Henzinger, Andreas Holzer, Christoph M. Kirsch, Michael Lippautz, Hannes Payer, Ali Sezgin, Ana Sokolova, and Helmut Veith. Local Linearizability for Concurrent Container-Type Data Structures. In 27th International Conference on Concurrency Theory (CONCUR 2016), volume 59 of Leibniz International Proceedings in Informatics (LIPIcs), pages 6:1-6:15, Dagstuhl, Germany, August 2016. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik. [ bib | DOI | .pdf | Abstract ]
[18] Victor B. F. Gomes and Georg Struth. Program construction and verification components based on Kleene algebra. Archive of Formal Proofs, 2016, June 2016. [ bib | http | Abstract ]
[19] Pedro da Rocha Pinto, Thomas Dinsdale-Young, Philippa Gardner, and Julian Sutherland. Modular termination verification for non-blocking concurrency. In ESOP 2016: Proceedings of the 25th European Symposium on Programming, pages 176-201, April 2016. [ bib | DOI | http | .pdf | Abstract ]
[20] Kasper Svendsen, Filip Sieczkowski, and Lars Birkedal. Transfinite step-indexing: Decoupling concrete and logical steps. In ESOP 2016, pages 727-751, April 2016. [ bib | DOI | http | .pdf | Abstract ]
[21] Victor B. F. Gomes, Walter Guttmann, Peter Höfner, Georg Struth, and Tjark Weber. Kleene algebras with domain. Archive of Formal Proofs, 2016, April 2016. [ bib | http | Abstract ]
[22] David Kaloper-Meršinjak and Hannes Mehnert. Not-quite-so-broken TLS 1.3 mechanised conformance checking. In TLSv1.3 - Ready or Not? (TRON) workshop, February 2016. [ bib | .pdf | Abstract ]
[23] David Kaloper-Meršinjak and Jeremy Yallop. Generic partially-static data (extended abstract). In Proceedings of the 1st International Workshop on Type-Driven Development, TyDe 2016, pages 39-40, New York, NY, USA, 2016. ACM. [ bib | DOI | http | http | Abstract ]
[24] Gian Ntzik, Pedro da Rocha Pinto, and Philippa Gardner. Fault-tolerant Resource Reasoning. In APLAS 2015: Proceedings of the 13th Asian Symposium on Programming Languages and Systems, pages 169-188, December 2015. [ bib | DOI | http | .pdf | Abstract ]
[25] Tom Ridge, David Sheets, Thomas Tuerk, Andrea Giugliano, Anil Madhavapeddy, and Peter Sewell. SibylFS: formal specification and oracle-based testing for POSIX and real-world file systems. In SOSP 2015: Proceedings of the 25th Symposium on Operating Systems Principles, Monterey, CA, USA, pages 38-53, October 2015. [ bib | DOI | http | .pdf | Abstract ]
[26] Gian Ntzik and Philippa Gardner. Reasoning about the POSIX File System: Local Update and Global Pathnames. In OOPSLA 2015: Proceedings of the 30th Annual ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications, October 2015. [ bib | Abstract ]
[27] David Kaloper-Mersinjak, Hannes Mehnert, Anil Madhavapeddy, and Peter Sewell. Not-quite-so-broken TLS: lessons in re-engineering a security protocol specification and implementation. In USENIX Security 2015: 24th USENIX Security Symposium, Washington, D.C., USA, pages 223-238, August 2015. [ bib | http | .pdf | Abstract ]
[28] Ali Sezgin and Serdar Tasiran. Moving around: Lipton's reduction for TSO - (regular submission). In VSTTE 2015: Verified Software: Theories, Tools, and Experiments - 7th International Conference, San Francisco, CA, USA. Revised Selected Papers, pages 165-182, July 2015. [ bib | DOI | http | Abstract ]
[29] Pedro da Rocha Pinto, Thomas Dinsdale-Young, and Philippa Gardner. Steps in Modular Specifications for Concurrent Modules (Invited Tutorial Paper). In MFPS 2015: Proceedings of the 31st Conference on the Mathematical Foundations of Programming Semantics, pages 3-18, June 2015. [ bib | DOI | http | .pdf | Abstract ]
[30] David Kaloper Meršinjak, Hannes Mehnert, Anil Madhavapeddy, and Peter Sewell. Not-quite-so-broken TLS: lessons in re-engineering a security protocol specification and implementation, May 2015. Presentation at HCSS 2015: the Fifteenth Annual High Confidence Software and Systems Conference. [ bib | Abstract ]
[31] Filip Sieczkowski, Kasper Svendsen, Lars Birkedal, and Jean Pichon-Pharabod. A separation logic for fictional sequential consistency. In ESOP 2015, April 2015. [ bib | DOI | Abstract ]
[32] Azalea Raad, Jules Villard, and Philippa Gardner. CoLoSL: Concurrent local subjective logic. In ESOP 2015, April 2015. [ bib | DOI | .pdf | Abstract ]
[33] Soham Chakraborty, Thomas A. Henzinger, Ali Sezgin, and Viktor Vafeiadis. Aspect-oriented linearizability proofs. Logical Methods in Computer Science, 11(1):1-33, April 2015. [ bib | DOI | http | Abstract ]
[34] David Kaloper Meršinjak and Hannes Mehnert. Trustworthy secure modular operating system engineering. Invited talk at 31st Chaos Communication Congress (31C3), January 2015. [ bib | Abstract ]
[35] Hannes Mehnert and David Kaloper Mersinjak. Transport Layer Security purely in OCaml. In Proceedings of the ACM OCaml 2014 Workshop, September 2014. [ bib | .pdf | Abstract ]
[36] Pedro da Rocha Pinto, Thomas Dinsdale-Young, and Philippa Gardner. TaDA: A logic for time and data abstraction. In Richard Jones, editor, ECOOP 2014, volume 8586 of Lecture Notes in Computer Science, pages 207-231. Springer Berlin Heidelberg, July 2014. [ bib | DOI | http | Abstract ]
[37] Philippa Gardner, Azalea Raad, Mark J. Wheelhouse, and Adam Wright. Abstract local reasoning for concurrent libraries: Mind the gap. MFPS 2014: Electr. Notes Theor. Comput. Sci., 308:147-166, June 2014. [ bib | DOI | http | Abstract ]
[38] Philippa Gardner, Gian Ntzik, and Adam Wright. Local reasoning for the POSIX file system. In ESOP 2014: Programming Languages and Systems - 23rd European Symposium on Programming, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Grenoble, France, pages 169-188, April 2014. [ bib | DOI | http | Abstract ]
[39] Tony Hoare, Stephan van Staden, Bernhard Möller, Georg Struth, Jules Villard, Huibiao Zhu, and Peter W. O'Hearn. Developments in concurrent Kleene algebra. In RAMiCS 2014: Relational and Algebraic Methods in Computer Science - 14th International Conference, Marienstatt, Germany, pages 1-18, April 2014. [ bib | DOI | http | Abstract ]

This file was generated by bibtex2html 1.96.