Task 3 Papers

[1] Robert N. M. Watson, Alexander Richardson, Brooks Davis, John Baldwin, David Chisnall, Jessica Clarke, Nathaniel Filardo, Simon W. Moore, Edward Napierala, Peter Sewell, and Peter G. Neumann. CHERI C/C++ Programming Guide. Technical Report UCAM-CL-TR-947, University of Cambridge, Computer Laboratory, June 2020. [ bib | .pdf | Abstract ]
[2] Nathaniel Wesley Filardo, Brett F. Gutstein, Jonathan Woodruff, Sam Ainsworth, Lucian Paul-Trifu, Brooks Davis, Hongyan Xia, Edward Tomasz Napierala, Alexander Richardson, John Baldwin, David Chisnall, Jessica Clarke, Khilan Gudka, Alexandre Joannou, A. Theodore Markettos, Alfredo Mazzinghi, Robert M. Norton, Michael Roe, Peter Sewell, Stacey Son, Timothy M. Jones, Simon W. Moore, Peter G. Neumann, , and Robert N. M. Watson. Cornucopia: Temporal safety for CHERI heaps. In Security and Privacy 2020: Proceedings of the 41st IEEE Symposium on Security and Privacy (SP), pages 1507--1524, Los Alamitos, CA, USA, may 2020. IEEE Computer Society. [ bib | DOI | .pdf | Abstract ]
[3] Shale Xiong. Parametric Operational Semantics for Consistency Models. PhD thesis, Imperial College London, 2020. [ bib | Abstract ]
[4] Gabriela Sampaio, José Fragoso Santos, Petar Maksimovic, and Philippa Gardner. A trusted infrastructure for symbolic analysis of event-driven web applications. In ECOOP 2020: 34th European Conference on Object-Oriented Programming, 2020. [ bib | Abstract ]
[5] José Fragoso Santos, Petar Maksimovic, Sacha-Élie Ayoun, and Philippa Gardner. Gillian, part i: A multi-language platform for symbolic execution. In PLDI 2020: Proceedings of the 41st ACM SIGPLAN International Conference on Programming Language Design and Implementation, 2020. [ bib | DOI | Abstract ]
[6] Shale Xiong, Andrea Cerone, Azalea Raad, and Philippa Gardner. Data consistency in transactional storage systems: a centralised approach. In ECOOP 2020: 34th European Conference on Object-Oriented Programming, 2020. [ bib | Abstract ]
[7] Conrad Watt, Andreas Rossberg, and Jean Pichon-Pharabod. Weakening WebAssembly. In OOPSLA 2019: Proceedings of the ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications, October 2019. Proc. ACM Program. Lang. 3, OOPSLA, Article 133. [ bib | DOI | http | Abstract ]
[8] Conrad Watt, Petar Maksimovic, Neelakantan R. Krishnaswami, and Philippa Gardner. A program logic for first-order encapsulated WebAssembly. In ECOOP 2019: Proceedings of the 33 rd European Conference on Object-Oriented Programming)., page 10:1–10:30, July 2019. [ bib | DOI | Abstract ]
[9] Stella Lau, Victor B. F. Gomes, Kayvan Memarian, Jean Pichon-Pharabod, and Peter Sewell. Cerberus-BMC: a principled reference semantics and exploration tool for concurrent and sequential C. In CAV 2019: Proc. 31st International Conference on Computer-Aided Verification, July 2019. (tool paper). [ bib | .pdf | Abstract ]
[10] Brooks Davis, Robert N. M. Watson, Alexander Richardson, Peter G. Neumann, Simon W. Moore, John Baldwin, David Chisnall, James Clarke, Nathaniel Wesley Filardo, Khilan Gudka, Alexandre Joannou, Ben Laurie, A. Theodore Markettos, J. Edward Maste, Alfredo Mazzinghi, Edward Tomasz Napierala, Robert M. Norton, Michael Roe, Peter Sewell, Stacey Son, and Jonathan Woodruff. CheriABI: Enforcing valid pointer provenance and minimizing pointer privilege in the POSIX C run-time environment. In ASPLOS 2019: the 24th ACM International Conference on Architectural Support for Programming Languages and Operating Systems. ACM, April 2019. Best paper award. [ bib | DOI | http | .pdf | Abstract ]
[11] José Fragoso Santos, Petar Maksimović, Gabriela Sampaio, and Philippa Gardner. JaVerT 2.0: Compositional symbolic execution for JavaScript. In POPL 2019: Proc. 46th ACM SIGPLAN Symposium on Principles of Programming Languages, January 2019. [ bib | .pdf | Abstract ]
[12] Conrad Watt, John Renner, Natalie Popescu, Sunjay Cauligi, and Deian Stefan. CT-Wasm: Type-driven secure cryptography for the web ecosystem. In POPL 2019: Proc. 46th ACM SIGPLAN Symposium on Principles of Programming Languages, January 2019. [ bib | .pdf | Abstract ]
[13] Kayvan Memarian, Victor B. F. Gomes, Brooks Davis, Stephen Kell, Alexander Richardson, Robert N. M. Watson, and Peter Sewell. Exploring C semantics and pointer provenance. In POPL 2019: Proc. 46th ACM SIGPLAN Symposium on Principles of Programming Languages, January 2019. Proc. ACM Program. Lang. 3, POPL, Article 67. [ bib | DOI | .pdf | Abstract ]
[14] Stephen Dolan, KC Sivaramakrishnan, and Anil Madhavapeddy. Bounding data races in space and time. In PLDI 2018: Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2018, pages 242--255, New York, NY, USA, June 2018. ACM. [ bib | DOI | http | .pdf | Abstract ]
[15] Arthur Charguéraud, Alan Schmitt, and Thomas Wood. JSExplain: a double debugger for JavaScript. In WWW '18 Companion: The 2018 Web Conference Companion, April 23--27, 2018, Lyon, France. ACM, April 2018. [ bib | DOI | .pdf | Abstract ]
[16] Kayvan Memarian, Victor Gomes, and Peter Sewell. N2263 sewell,clarifying pointer provenance (q1-q20) v4. ISO SC22 WG14 N2263, March 2018. [ bib ]
[17] Kayvan Memarian, Victor Gomes, and Peter Sewell. N2223: Clarifying the c memory object model: Introduction to n2219 -- n2222. ISO SC22 WG14 N2223, March 2018. [ bib ]
[18] Kayvan Memarian, Victor Gomes, and Peter Sewell. N2222: Further pointer issues (q21-q46). ISO SC22 WG14 N2222, March 2018. [ bib ]
[19] Kayvan Memarian, Victor Gomes, and Peter Sewell. N2221: Clarifying unspecified values (q48-q59) v3. ISO SC22 WG14 N2221, March 2018. [ bib ]
[20] Kayvan Memarian, Victor Gomes, and Peter Sewell. N2220: Clarifying trap representations (q47) v3. ISO SC22 WG14 N2220, March 2018. [ bib ]
[21] Kayvan Memarian, Victor Gomes, and Peter Sewell. N2219: Clarifying pointer provenance (q1-q20) v3. ISO SC22 WG14 N2219, March 2018. [ bib ]
[22] Jean Pichon-Pharabod. A no-thin-air memory model for programming languages. PhD thesis, University of Cambridge, 2018. [ bib | Abstract ]
[23] José Fragoso Santos, Petar Maksimović, Daiva Naudžiunienė, Thomas Wood, and Philippa Gardner. JaVerT: JavaScript verification toolchain. In POPL 2018, January 2018. [ bib | DOI | .pdf | Abstract ]
[24] Conrad Watt. Mechanising and verifying the WebAssembly specification. In CPP 2018: Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2018, pages 53--65, New York, NY, USA, 2018. ACM. [ bib | DOI | http | .pdf | Abstract ]
[25] Stephen Kell. Some were meant for C: the endurance of an unmanageable language. In Onward! 2017: Proceedings of the 2017 ACM International Symposium on New Ideas, New Paradigms, and Reflections on Programming & Software, Onward! 2017, New York, NY, USA, October 2017. ACM. [ bib | DOI | .pdf | Abstract ]
[26] Jeremy Yallop, David Sheets, and Anil Madhavapeddy. A modular foreign function interface. Science of Computer Programming, April 2017. [ bib | DOI | http | .pdf | Abstract ]
[27] David Chisnall, Brooks Davis, Khilan Gudka, David Brazdil, Alexandre Joannou, Jonathan Woodruff, A. Theodore Markettos, J. Edward Maste, Robert Norton, Stacey Son, Michael Roe, Simon W. Moore, Peter G. Neumann, Ben Laurie, and Robert N.M. Watson. CHERI JNI: Sinking the Java Security Model into the C. In ASPLOS 2017: Proceedings of the Twenty-Second International Conference on Architectural Support for Programming Languages and Operating Systems, ASPLOS '17, pages 569--583, New York, NY, USA, April 2017. ACM. [ bib | DOI | http | Abstract ]
[28] Anthony C. J. Fox, Magnus O. Myreen, Yong Kiam Tan, and Ramana Kumar. Verified compilation of CakeML to multiple machine-code targets. In Yves Bertot and Viktor Vafeiadis, editors, Proc. CPP 2017: Certified Programs and Proofs. ACM, January 2017. [ bib | DOI | .pdf | Abstract ]
[29] Kyndylan Nienhuis, Kayvan Memarian, and Peter Sewell. An operational semantics for C/C++11 concurrency. In OOPSLA 2016: Proceedings of the ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications, New York, NY, USA, November 2016. ACM. [ bib | .pdf | Abstract ]
[30] Stephen Kell, Dominic P. Mulligan, and Peter Sewell. The missing link: explaining ELF static linking, semantically. In OOPSLA 2016: Proceedings of the ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2016, New York, NY, USA, November 2016. ACM. [ bib | .pdf | Abstract ]
[31] Stephen Kell. Dynamically diagnosing type errors in unsafe code. In OOPSLA 2016: Proceedings of the ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2016, New York, NY, USA, November 2016. ACM. [ bib | .pdf | Abstract ]
[32] Yong Kiam Tan, Magnus O. Myreen, Ramana Kumar, Anthony Fox, Scott Owens, and Michael Norrish. A new verified compiler backend for CakeML. In Proc. ICFP 2016: International Conference on Functional Programming. ACM Press, September 2016. [ bib | DOI | .pdf | Abstract ]
[33] Kayvan Memarian and Peter Sewell. Clarifying trap representations (draft defect report or proposal for c2x). ISO SC22 WG14 N2091, September 2016. [ bib ]
[34] Kayvan Memarian and Peter Sewell. Clarifying pointer provenance (draft defect report or proposal for c2x). ISO SC22 WG14 N2090, September 2016. [ bib ]
[35] Kayvan Memarian and Peter Sewell. Clarifying unspecified values (draft defect report or proposal for c2x). ISO SC22 WG14 N2089, September 2016. [ bib ]
[36] Kayvan Memarian, Justus Matthiesen, James Lingard, Kyndylan Nienhuis, David Chisnall, Robert N.M. Watson, and Peter Sewell. Into the depths of C: elaborating the de facto standards. In PLDI 2016, June 2016. PLDI 2016 Distinguished Paper award. [ bib | .pdf | Abstract ]
[37] Kayvan Memarian and Peter Sewell. What is C in practice? (Cerberus survey v2): Analysis of responses -- with comments. ISO SC22 WG14 N2015, March 2016. [ bib | .txt ]
[38] Kayvan Memarian and Peter Sewell. What is C in practice? (Cerberus survey v2): Analysis of responses. ISO SC22 WG14 N2014, March 2016. [ bib ]
[39] David Chisnall, Justus Matthiesen, Kayvan Memarian, Kyndylan Nienhuis, Peter Sewell, and Robert N. M. Watson. C memory object and value semantics: the space of de facto and ISO standards. ISO SC22 WG14 N2013, March 2016. [ bib | .pdf ]
[40] Kayvan Memarian and Peter Sewell. Clarifying the C memory object model. ISO SC22 WG14 N2012, March 2016. [ bib ]
[41] Jean Pichon-Pharabod and Peter Sewell. A concurrency semantics for relaxed atomics that permits optimisation and avoids thin-air executions. In POPL 2016: Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, St. Petersburg, FL, USA, January 20 - 22, 2016, pages 622--633, January 2016. [ bib | DOI | http | .pdf | Abstract ]
[42] Stephen Kell. Towards a dynamic object model within Unix processes. In Onward! 2015: 2015 ACM International Symposium on New Ideas, New Paradigms, and Reflections on Programming and Software, Pittsburgh, PA, USA, pages 224--239, October 2015. [ bib | DOI | http | .pdf | Abstract ]
[43] Khilan Gudka, Robert N. M. Watson, Jonathan Anderson, David Chisnall, Brooks Davis, Ben Laurie, Ilias Marinos, Peter G. Neumann, and Alex Richardson. Clean Application Compartmentalization with SOAAP. In CCS 2015: Proceedings of the 22nd ACM Conference on Computer and Communications Security, October 2015. [ bib | .pdf | Abstract ]
[44] Kayvan Memarian, Kyndylan Nienhuis, Justus Matthiesen, James Lingard, and Peter Sewell. Cerberus: towards an executable semantics for sequential and concurrent C11, May 2015. Presentation at HCSS 2015: the Fifteenth Annual High Confidence Software and Systems Conference. [ bib | Abstract ]
[45] Mark Batty, Kayvan Memarian, Kyndylan Nienhuis, Jean Pichon-Pharabod, and Peter Sewell. The problem of programming language concurrency semantics. In ESOP 2015: Programming Languages and Systems - 24th European Symposium on Programming, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11-18, 2015., pages 283--307, April 2015. [ bib | DOI | http | .pdf | Abstract ]
[46] David Chisnall, Colin Rothwell, Brooks Davis, Robert N.M. Watson, Jonathan Woodruff, Munraj Vadera, Simon W. Moore, Peter G. Neumann, and Michael Roe. Beyond the PDP-11: Processor support for a memory-safe C abstract machine. In ASPLOS 2015: Proceedings of the Fifteenth Edition of ASPLOS on Architectural Support for Programming Languages and Operating Systems, ASPLOS XX, New York, NY, USA, March 2015. ACM. [ bib | DOI | Abstract ]
[47] Mark John Batty. The C11 and C++11 Concurrency Model. PhD thesis, University of Cambridge Computer Laboratory, November 2014. Winner of 2015 ACM SIGPLAN John C. Reynolds Doctoral Dissertation Award and 2015 CPHC/BCS Distinguished Dissertation competition. [ bib ]
[48] Stephen Kell. In search of types. In Onward! 2014: Proceedings of the 2014 ACM International Symposium on New Ideas, New Paradigms, and Reflections on Programming & Software, Onward! 2014, pages 227--241, New York, NY, USA, October 2014. ACM. [ bib | DOI | http | Abstract ]
[49] Reinoud Elhorst, Mark Batty, and David Chisnall. Efficient code generation for weakly ordered architectures. Presentation at the 4th European LLVM conference (EuroLLVM), April 2014. Slides and report available at http://llvm.org/devmtg/2014-04/. [ bib | Abstract ]
[50] Reinoud Elhorst. Lowering C11 atomics for ARM in LLVM, March 2014. [ bib | .pdf | Abstract ]
[51] Magnus O. Myreen and Scott Owens. Proof-producing translation of higher-order logic into pure and stateful ML. J. Funct. Program., 24(2-3):284--315, January 2014. [ bib | DOI | http | Abstract ]
[52] Ramana Kumar, Magnus O. Myreen, Michael Norrish, and Scott Owens. CakeML: a verified implementation of ML. In POPL 2014: The 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, San Diego, CA, USA, pages 179--192, January 2014. [ bib | DOI | http | Abstract ]
[53] Gabriel Kerneis, Charlie Shepherd, and Stefan Hajnoczi. QEMU/CPC: static analysis and CPS conversion for safe, portable, and efficient coroutines. In PEPM 2014: Proceedings of the ACM SIGPLAN 2014 workshop on Partial evaluation and program manipulation, San Diego, California, USA, pages 83--94, January 2014. [ bib | DOI | http | Abstract ]

This file was generated by bibtex2html 1.99.