[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] Kyndylan Nienhuis, Alexandre Joannou, Thomas Bauereiss, Anthony Fox, Michael Roe, Brian Campbell, Matthew Naylor, Robert M. Norton, Simon W. Moore, Peter G. Neumann, Ian Stark, Robert N. M. Watson, and Peter Sewell. Rigorous engineering for hardware security: Formal modelling and proof in the CHERI design and implementation process. In Security and Privacy 2020: Proceedings of the 41st IEEE Symposium on Security and Privacy (SP), May 2020. [ bib | .pdf | Abstract ]
[4] Ben Simner, Shaked Flur, Christopher Pulte, Alasdair Armstrong, Jean Pichon-Pharabod, Luc Maranget, and Peter Sewell. ARMv8-A system semantics: instruction fetch in relaxed architectures (extended version). In ESOP 2020: Proceedings of the 29th European Symposium on Programming, April 2020. This is an extended version of the ESOP 2020 paper, with appendices giving additional details. [ bib | .pdf | Abstract ]
[5] Shale Xiong. Parametric Operational Semantics for Consistency Models. PhD thesis, Imperial College London, 2020. [ bib | Abstract ]
[6] 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 ]
[7] 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 ]
[8] 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 ]
[9] 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 ]
[10] J. Woodruff, A. Joannou, H. Xia, A. Fox, R. M. Norton, D. Chisnall, B. Davis, K. Gudka, N. W. Filardo, A. T. Markettos, M. Roe, P. G. Neumann, R. N. M. Watson, and S. W. Moore. Cheri concentrate: Practical compressed capabilities. IEEE Transactions on Computers, 68(10):1455--1469, October 2019. [ bib | DOI | .pdf | Abstract ]
[11] Robert N. M. Watson, Simon W. Moore, Peter Sewell, and Peter Neumann. An introduction to CHERI. Technical Report UCAM-CL-TR-941, University of Cambridge, Computer Laboratory, September 2019. [ bib | .pdf | Abstract ]
[12] Kyndylan Nienhuis, Alexandre Joannou, Anthony Fox, Michael Roe, Thomas Bauereiss, Brian Campbell, Matthew Naylor, Robert M. Norton, Simon W. Moore, Peter G. Neumann, Ian Stark, Robert N. M. Watson, and Peter Sewell. Rigorous engineering for hardware security: Formal modelling and proof in the CHERI design and implementation process. Technical Report UCAM-CL-TR-940, University of Cambridge, Computer Laboratory, September 2019. [ bib | .pdf | Abstract ]
[13] 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 ]
[14] 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 ]
[15] Robert N. M. Watson, Peter G. Neumann, Jonathan Woodruff, Michael Roe, Hesham Almatary, Jonathan Anderson, John Baldwin, David Chisnall, Brooks Davis, Nathaniel Wesley Filardo, Alexandre Joannou, Ben Laurie, A. Theodore Markettos, Simon W. Moore, Steven J. Murdoch, Kyndylan Nienhuis, Robert Norton, Alex Richardson, Peter Rugg, Peter Sewell, Stacey Son, and Hongyan Xia. Capability Hardware Enhanced RISC Instructions: CHERI Instruction-Set Architecture (Version 7). Technical Report UCAM-CL-TR-927, University of Cambridge, Computer Laboratory, June 2019. [ bib | .pdf | Abstract ]
[16] Christopher Pulte, Jean Pichon-Pharabod, Jeehoon Kang, Sung-Hwan Lee, and Chung-Kil Hur. Promising-ARM/RISC-V: A simpler and faster operational concurrency model. In PLDI 2019: Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation, June 2019. [ bib | DOI | .pdf | Abstract ]
[17] 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 ]
[18] 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 ]
[19] 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 ]
[20] 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 ]
[21] 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. Technical Report UCAM-CL-TR-932, University of Cambridge, Computer Laboratory, January 2019. [ bib | .pdf | Abstract ]
[22] Alasdair Armstrong, Thomas Bauereiss, Brian Campbell, Alastair Reid, Kathryn E. Gray, Robert M. Norton, Prashanth Mundkur, Mark Wassell, Jon French, Christopher Pulte, Shaked Flur, Ian Stark, Neel Krishnaswami, and Peter Sewell. ISA semantics for ARMv8-A, RISC-V, and CHERI-MIPS. In POPL 2019: Proc. 46th ACM SIGPLAN Symposium on Principles of Programming Languages, January 2019. Proc. ACM Program. Lang. 3, POPL, Article 71. [ bib | DOI | .pdf | Abstract ]
[23] Martin Bodin, Philippa Gardner, Thomas Jensen, and Alan Schmitt. Skeletal semantics and their interpretations. In POPL 2019: Proc. 46th ACM SIGPLAN Symposium on Principles of Programming Languages, January 2019. [ bib | .pdf | Abstract ]
[24] Peter Sewell. REMS: Rigorous Engineering for Mainstream Systems. Summary 2013-03 -- 2019-01, January 2019. [ bib | .pdf | Abstract ]
[25] 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 ]
[26] Andrew Waterman and Krste Asanović, editors. The RISC-V Instruction Set Manual Volume I: Unprivileged ISA. December 2018. Document Version 20181221-Public-Review-draft. Contributors: Arvind, Krste Asanović, Rimas Avižienis, Jacob Bachmeyer, Christopher F. Batten, Allen J. Baum, Alex Bradbury, Scott Beamer, Preston Briggs, Christopher Celio, Chuanhua Chang, David Chisnall, Paul Clayton, Palmer Dabbelt, Roger Espasa, Shaked Flur, Stefan Freudenberger, Jan Gray, Michael Hamburg, John Hauser, David Horner, Bruce Hoult, Alexandre Joannou, Olof Johansson, Ben Keller, Yunsup Lee, Paul Loewenstein, Daniel Lustig, Yatin Manerkar, Luc Maranget, Margaret Martonosi, Joseph Myers, Vijayanand Nagarajan, Rishiyur Nikhil, Jonas Oberhauser, Stefan O'Rear, Albert Ou, John Ousterhout, David Patterson, Christopher Pulte, Jose Renau, Colin Schmidt, Peter Sewell, Susmit Sarkar, Michael Taylor, Wesley Terpstra, Matt Thomas, Tommy Thorn, Caroline Trippel, Ray VanDeWalker, Muralidaran Vijayaraghavan, Megan Wachs, Andrew Waterman, Robert Watson, Derek Williams, Andrew Wright, Reinoud Zandijk, and Sizhuo Zhang. [ bib | .pdf ]
[27] 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 ]
[28] 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 ]
[29] 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 ]
[30] 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 ]
[31] 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 ]
[32] Kayvan Memarian, Victor Gomes, and Peter Sewell. N2263 sewell,clarifying pointer provenance (q1-q20) v4. ISO SC22 WG14 N2263, March 2018. [ bib ]
[33] 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 ]
[34] Kayvan Memarian, Victor Gomes, and Peter Sewell. N2222: Further pointer issues (q21-q46). ISO SC22 WG14 N2222, March 2018. [ bib ]
[35] Kayvan Memarian, Victor Gomes, and Peter Sewell. N2221: Clarifying unspecified values (q48-q59) v3. ISO SC22 WG14 N2221, March 2018. [ bib ]
[36] Kayvan Memarian, Victor Gomes, and Peter Sewell. N2220: Clarifying trap representations (q47) v3. ISO SC22 WG14 N2220, March 2018. [ bib ]
[37] Kayvan Memarian, Victor Gomes, and Peter Sewell. N2219: Clarifying pointer provenance (q1-q20) v3. ISO SC22 WG14 N2219, March 2018. [ bib ]
[38] 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 ]
[39] 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 ]
[40] Jean Pichon-Pharabod. A no-thin-air memory model for programming languages. PhD thesis, University of Cambridge, 2018. [ bib | Abstract ]
[41] 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 ]
[42] 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 ]
[43] Christopher Pulte, Shaked Flur, Will Deacon, Jon French, Susmit Sarkar, and Peter Sewell. Simplifying ARM Concurrency: Multicopy-atomic Axiomatic and Operational Models for ARMv8. In POPL 2018, pages 19:1--19:29, January 2018. [ bib | DOI | http | .pdf | Abstract ]
[44] 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 ]
[45] 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 ]
[46] Alexandre Joannou, Jonathan Woodruff, Robert Kovacsics, Simon W. Moore, Alex Bradbury, Hongyan Xia, Robert N. M. Watson, David Chisnall, Michael Roe, Brooks Davis, Edward Napierala, John Baldwin, Khilan Gudka, Peter G. Neumann, Alfredo Mazzinghi, Alex Richardson, Stacey Son, and A. Theodore Markettos. Efficient tagged memory. In ICCD 2017: IEEE 35th International Conference on Computer Design, November 2017. [ bib | DOI | www: | .pdf | Abstract ]
[47] 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 ]
[48] 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 ]
[49] Philippa Gardner. Verified trustworthy software systems. Philosophical Transactions of the Royal Society of London A, 375(2104), September 2017. [ bib | DOI | .pdf | Abstract ]
[50] 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 ]
[51] 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 ]
[52] 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 ]
[53] 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 ]
[54] Jeremy Yallop, David Sheets, and Anil Madhavapeddy. A modular foreign function interface. Science of Computer Programming, April 2017. [ bib | DOI | http | .pdf | Abstract ]
[55] 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 ]
[56] Robert N. M. Watson, Peter G. Neumann, Jonathan Woodruff, Michael Roe, Jonathan Anderson, John Baldwin, David Chisnall, Brooks Davis, Alexandre Joannou, Ben Laurie, Simon W. Moore, Steven J. Murdoch, Robert Norton, Stacey Son, and Hongyan Xia. Capability Hardware Enhanced RISC Instructions: CHERI Instruction-Set Architecture (Version 6). Technical Report UCAM-CL-TR-907, University of Cambridge, Computer Laboratory, April 2017. [ bib | .pdf | Abstract ]
[57] 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 ]
[58] 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 ]
[59] 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 ]
[60] Shaked Flur, Susmit Sarkar, Christopher Pulte, Kyndylan Nienhuis, Luc Maranget, Kathryn E. Gray, Ali Sezgin, Mark Batty, and Peter Sewell. Mixed-size concurrency: ARM, POWER, C/C++11, and SC. In POPL 2017: The 44st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Paris, France, pages 429--442, January 2017. [ bib | DOI | http | .pdf | Abstract ]
[61] 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 ]
[62] 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 ]
[63] 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 ]
[64] 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 ]
[65] 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 ]
[66] 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 ]
[67] Brian Campbell and Ian Stark. Extracting behaviour from an executable instruction set model. In Ruzica Piskac and Muralidhar Talupur, editors, FMCAD 2016: Formal Methods in Computer-Aided Design, pages 33--40, October 2016. Full proceedings http://www.cs.utexas.edu/users/hunt/FMCAD/FMCAD16/proceedings/fmcad-2016-proceedings.pdf. [ bib | .pdf | Abstract ]
[68] Azalea Raad. Abstraction, Refinement and Concurrent Reasoning. PhD thesis, Imperial College London, September 2016. [ bib | .pdf | Abstract ]
[69] Pedro da Rocha Pinto. Reasoning with Time and Data Abstractions. PhD thesis, Imperial College London, September 2016. [ bib | .pdf | Abstract ]
[70] Gian Ntzik. Reasoning About POSIX File Systems. PhD thesis, Imperial College London, September 2016. [ bib | .pdf | Abstract ]
[71] 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 ]
[72] 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 ]
[73] Hannes Mehnert and Louis Gesbert. Conex --- establishing trust into data repositories. In Proceedings of the ACM OCaml 2016 Workshop, September 2016. [ bib | .pdf | Abstract ]
[74] 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 ]
[75] Kayvan Memarian and Peter Sewell. Clarifying trap representations (draft defect report or proposal for c2x). ISO SC22 WG14 N2091, September 2016. [ bib ]
[76] Kayvan Memarian and Peter Sewell. Clarifying pointer provenance (draft defect report or proposal for c2x). ISO SC22 WG14 N2090, September 2016. [ bib ]
[77] Kayvan Memarian and Peter Sewell. Clarifying unspecified values (draft defect report or proposal for c2x). ISO SC22 WG14 N2089, September 2016. [ bib ]
[78] Robert N.M. Watson, Robert M. Norton, Jonathan Woodruff, Simon W. Moore, Peter G. Neumann, Jonathan Anderson, David Chisnall, Brooks Davis, Ben Laurie, Michael Roe, Nirav H. Dave, Khilan Gudka, Alexandre Joannou, A. Theodore Markettos, Ed Maste, Steven J. Murdoch, Colin Rothwell, Stacey D. Son, and Munraj Vadera. Fast protection-domain crossing in the CHERI capability-system architecture. IEEE Micro, 36(5):38--49, September 2016. [ bib | DOI | http | Abstract ]
[79] M. Naylor, S. W. Moore, and A. Mujumdar. A consistency checker for memory subsystem traces. In FMCAD 2016: Formal Methods in Computer-Aided Design, September 2016. [ bib | DOI | .pdf | Abstract ]
[80] 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 ]
[81] 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 ]
[82] 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 ]
[83] 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 ]
[84] 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 ]
[85] 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 ]
[86] 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 ]
[87] Kayvan Memarian and Peter Sewell. What is C in practice? (Cerberus survey v2): Analysis of responses. ISO SC22 WG14 N2014, March 2016. [ bib ]
[88] 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 ]
[89] Kayvan Memarian and Peter Sewell. Clarifying the C memory object model. ISO SC22 WG14 N2012, March 2016. [ bib ]
[90] Brian Campbell and Ian Stark. Randomised testing of a microprocessor model using SMT-solver state generation. Sci. Comput. Program., 118:60--76, March 2016. [ bib | DOI | .pdf | Abstract ]
[91] 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 ]
[92] 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 ]
[93] Shaked Flur, Kathryn E. Gray, Christopher Pulte, Susmit Sarkar, Ali Sezgin, Luc Maranget, Will Deacon, and Peter Sewell. Modelling the ARMv8 architecture, operationally: concurrency and ISA. In POPL 2016: Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, St. Petersburg, FL, USA, pages 608--621, January 2016. [ bib | DOI | http | .pdf | Abstract ]
[94] 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 ]
[95] Kathryn E. Gray, Gabriel Kerneis, Dominic P. Mulligan, Christopher Pulte, Susmit Sarkar, and Peter Sewell. An integrated concurrency and core-ISA architectural envelope definition, and test oracle, for IBM POWER multiprocessors. In MICRO 2015: Proceedings of the 48th International Symposium on Microarchitecture, , Waikiki, HI, USA, pages 635--646, December 2015. [ bib | DOI | http | .pdf | Abstract ]
[96] 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 ]
[97] 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 ]
[98] 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 ]
[99] 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 ]
[100] Robert N. M. Watson, David Chisnall, Brooks Davis, Wojciech Koszek, Simon W. Moore, Steven J. Murdoch, Peter G. Neumann, and Jonathan Woodruff. Capability Hardware Enhanced RISC Instructions: CHERI Programmer's Guide. Technical Report UCAM-CL-TR-877, University of Cambridge, Computer Laboratory, September 2015. [ bib | .pdf | Abstract ]
[101] Robert N. M. Watson, Peter G. Neumann, Jonathan Woodruff, Michael Roe, Jonathan Anderson, David Chisnall, Brooks Davis, Alexandre Joannou, Ben Laurie, Simon W. Moore, Steven J. Murdoch, Robert Norton, and Stacey Son. Capability Hardware Enhanced RISC Instructions: CHERI Instruction-Set Architecture. Technical Report UCAM-CL-TR-876, University of Cambridge, Computer Laboratory, September 2015. [ bib | .pdf | Abstract ]
[102] Matthew Naylor and Simon W. Moore. A generic synthesisable test bench. In MEMOCODE 2015: ACM/IEEE International Conference on Formal Methods and Models for Codesign, Austin, TX, USA, pages 128--137, September 2015. [ bib | DOI | http | .pdf | Abstract ]
[103] 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 ]
[104] Anthony C. J. Fox. Improved tool support for machine-code decompilation in HOL4. In ITP 2015:Interactive Theorem Proving - 6th International Conference, Nanjing, China, pages 187--202, August 2015. [ bib | DOI | http | .pdf | Abstract ]
[105] 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 ]
[106] 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 ]
[107] 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 ]
[108] 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 ]
[109] Robert N. M. Watson, Jonathan Woodruff, Peter G. Neumann, Simon W. Moore, Jonathan Anderson, David Chisnall, Nirav Dave, Brooks Davis, Khilan Gudka, Ben Laurie, Steven J. Murdoch, Robert Norton, Michael Roe, Stacey Son, and Munraj Vadera. CHERI: A hybrid capability-system architecture for scalable software compartmentalization. In Security and Privacy 2015: Proceedings of the 36th IEEE Symposium on Security and Privacy (“Oakland”), May 2015. [ bib | DOI | .pdf | Abstract ]
[110] S. Flur, K. Gray, G. Kerneis, D. Mulligan, C. Pulte, S. Sarkar, and P. Sewell. Rigorous architectural modelling for production multiprocessors, May 2015. Presentation at HCSS 2015: the Fifteenth Annual High Confidence Software and Systems Conference. [ bib | Abstract ]
[111] 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 ]
[112] Azalea Raad, Jules Villard, and Philippa Gardner. CoLoSL: Concurrent local subjective logic. In ESOP 2015, April 2015. [ bib | DOI | .pdf | Abstract ]
[113] 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 ]
[114] 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 ]
[115] A. M. Pitts, J. Matthiesen, and J. Derikx. A dependent type theory with abstractable names. In I. Mackie and M. Ayala-Rincon, editors, LSFA 2014: Proceedings of the 9th Workshop on Logical and Semantic Frameworks, with Applications, volume 312 of Electronic Notes in Theoretical Computer Science, pages 19--50. Elsevier, April 2015. [ bib | DOI | http | Abstract ]
[116] 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 ]
[117] Jade Alglave, Mark Batty, Alastair F. Donaldson, Ganesh Gopalakrishnan, Jeroen Ketema, Daniel Poetzl, Tyler Sorensen, and John Wickerson. GPU concurrency: Weak behaviours and programming assumptions. In ASPLOS 2015: Proceedings of the Twentieth International Conference on Architectural Support for Programming Languages and Operating Systems, Istanbul, Turkey, pages 577--591, March 2015. [ bib | DOI | http | Abstract ]
[118] 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 ]
[119] 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 ]
[120] 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 ]
[121] 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 ]
[122] Brian Campbell and Ian Stark. Randomised testing of a microprocessor model using SMT-solver state generation. In Frédéric Lang and Francesco Flammini, editors, FMICS 2014: Formal Methods for Industrial Critical Systems, volume 8718 of Lecture Notes in Computer Science, pages 185--199. Springer, September 2014. [ bib | DOI | .pdf | Abstract ]
[123] Dominic P. Mulligan, Scott Owens, Kathryn E. Gray, Tom Ridge, and Peter Sewell. Lem: Reusable engineering of real-world semantics. In ICFP 2014: Proceedings of the 19th ACM SIGPLAN International Conference on Functional Programming, pages 175--188, New York, NY, USA, September 2014. ACM. [ bib | DOI | http | .pdf | Abstract ]
[124] Basile Clement. Running programming language specifications, August 2014. MPRI report. [ bib ]
[125] 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 ]
[126] 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 ]
[127] 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 ]
[128] 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 ]
[129] 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 ]
[130] Reinoud Elhorst. Lowering C11 atomics for ARM in LLVM, March 2014. [ bib | .pdf | Abstract ]
[131] 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 ]
[132] 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 ]
[133] 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.