Task 4 Papers

[1] Steve Bishop, Matthew Fairbairn, Hannes Mehnert, Michael Norrish, Tom Ridge, Peter Sewell, Michael Smith, and Keith Wansbrough. Engineering with logic: Rigorous test-oracle specification and validation for TCP/IP and the Sockets API. J. ACM, 66(1):1:1--1:77, December 2018. [ bib | DOI | http | .pdf | Abstract ]
[2] José Fragoso Santos, Petar Maksimovic, Théotime Grohens, Julian Dolby, and Philippa Gardner. Symbolic execution for JavaScript. In PPDP 2018: Proceedings of the 20th International Symposium on Principles and Practice of Declarative Programming, pages 11:1--11:14, September 2018. [ bib | DOI | http | www: | Abstract ]
[3] Thomas Dinsdale-Young, Pedro da Rocha Pinto, and Philippa Gardner. A perspective on specifying and verifying concurrent modules. Journal of Logical and Algebraic Methods in Programming, 98:1--25, August 2018. [ bib | DOI | http | .pdf | Abstract ]
[4] Gian Ntzik, Pedro da Rocha Pinto, Julian Sutherland, and Philippa Gardner. A concurrent specification of POSIX file systems. In ECOOP 2018: 32nd European Conference on Object-Oriented Programming, July 2018. [ bib | DOI | .pdf | Abstract ]
[5] Kasper Svendsen, Jean Pichon-Pharabod, Marko Doko, Ori Lahav, and Viktor Vafeiadis. A separation logic for a promising semantics. In ESOP 2018, 2018. [ bib | .pdf | Abstract ]
[6] Brijesh Dongol, Radha Jagadeesan, James Riely, and Alasdair Armstrong. On abstraction and compositionality for weak-memory linearisability. In Isil Dillig and Jens Palsberg, editors, VMCAI 2018: Verification, Model Checking, and Abstract Interpretation - 19th International Conference, LNCS, pages 183--204. Springer, January 2018. [ bib | DOI | http | Abstract ]
[7] Thomas Bauereiß, Armando Pesenti Gritti, Andrei Popescu, and Franco Raimondi. Cosmed: A confidentiality-verified social media platform. J. Automated Reasoning, December 2017. [ bib | DOI | http | Abstract ]
[8] 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, November 2017. [ bib | DOI | http | Abstract ]
[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), pages 109:1--109:28, October 2017. Distinguished Paper award. [ bib | DOI | http | Abstract ]
[10] 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 ]
[11] Philippa Gardner. Verified trustworthy software systems. Philosophical Transactions of the Royal Society of London A, 375(2104), September 2017. [ bib | DOI | .pdf | Abstract ]
[12] José Fragoso Santos, Philippa Gardner, Petar Maksimovic, and Daiva Naudziuniene. Towards logic-based verification of JavaScript programs. In Leonardo de Moura, editor, CADE 2017: 26th International Conference on Automated Deduction, volume 10395 of Lecture Notes in Computer Science, pages 8--25. Springer, August 2017. [ bib | DOI | .html | Abstract ]
[13] 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 ]
[14] 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 ]
[15] Lars Birkedal, Thomas Dinsdale-Young, Guilhem Jaber, Kasper Svendsen, and Nikos Tzevelekos. Trace properties from separation logic specifications. CoRR, abs/1702.02972, February 2017. [ bib | http | http | Abstract ]
[16] 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 ]
[17] 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 ]
[18] 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 ]
[19] 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 ]
[20] Hannes Mehnert and Louis Gesbert. Conex --- establishing trust into data repositories. In Proceedings of the ACM OCaml 2016 Workshop, September 2016. [ bib | .pdf | Abstract ]
[21] 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 ]
[22] 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, September 2016. ACM. [ bib | DOI | http | http | Abstract ]
[23] Gian Ntzik. Reasoning About POSIX File Systems. PhD thesis, Imperial College London, September 2016. [ bib | .pdf | Abstract ]
[24] Pedro da Rocha Pinto. Reasoning with Time and Data Abstractions. PhD thesis, Imperial College London, September 2016. [ bib | .pdf | Abstract ]
[25] Azalea Raad. Abstraction, Refinement and Concurrent Reasoning. PhD thesis, Imperial College London, September 2016. [ bib | .pdf | Abstract ]
[26] 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 ]
[27] 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 ]
[28] 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 ]
[29] 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 ]
[30] 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 ]
[31] 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 ]
[32] 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 ]
[33] 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 ]
[34] 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 ]
[35] 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 ]
[36] 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 ]
[37] 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 ]
[38] 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 ]
[39] 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 ]
[40] Azalea Raad, Jules Villard, and Philippa Gardner. CoLoSL: Concurrent local subjective logic. In ESOP 2015, April 2015. [ bib | DOI | .pdf | Abstract ]
[41] 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 ]
[42] 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 ]
[43] 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 ]
[44] 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 ]
[45] 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 ]
[46] 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 ]
[47] 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.98.