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] | 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 ] |
[6] | 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 ] |
[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] | Philippa Gardner. Verified trustworthy software systems. Philosophical Transactions of the Royal Society of London A, 375(2104), September 2017. [ bib | DOI | .pdf | Abstract ] |
[11] | 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 ] |
[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] | 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 ] |
[14] | 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 ] |
[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] | 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 ] |
[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] | 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 ] |
[20] | Azalea Raad. Abstraction, Refinement and Concurrent Reasoning. PhD thesis, Imperial College London, September 2016. [ bib | .pdf | Abstract ] |
[21] | Pedro da Rocha Pinto. Reasoning with Time and Data Abstractions. PhD thesis, Imperial College London, September 2016. [ bib | .pdf | Abstract ] |
[22] | Gian Ntzik. Reasoning About POSIX File Systems. PhD thesis, Imperial College London, September 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, September 2016. ACM. [ bib | DOI | http | http | Abstract ] |
[24] | 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 ] |
[25] | Hannes Mehnert and Louis Gesbert. Conex --- establishing trust into data repositories. In Proceedings of the ACM OCaml 2016 Workshop, 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] | 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 ] |
[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] | 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 ] |
[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] | 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 ] |
[34] | 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 ] |
[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] | 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 ] |
[40] | Azalea Raad, Jules Villard, and Philippa Gardner. CoLoSL: Concurrent local subjective logic. In ESOP 2015, April 2015. [ bib | DOI | .pdf | Abstract ] |
[41] | 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 ] |
[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] | 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 ] |
[47] | 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 ] |
This file was generated by bibtex2html 1.99.