@online{DepartmentComputerScience,
    title       = {{{CHERI}}: {{The Arm Morello Board}}},
    url         = {https://www.cl.cam.ac.uk/research/security/ctsrd/cheri/cheri-morello.html}
}

@online{DigitalSecurityDesign,
    title       = {{Digital Security by Design Challenge \textendash{} {{UKRI}}}},
    url         = {https://www.ukri.org/our-work/our-main-funds/industrial-strategy-challenge-fund/artificial-intelligence-and-data-economy/digital-security-by-design-challenge/}
}

@online{DepartmentComputerScienceb,
    title       = {{{CHERI}}: {{The Digital Security}} by {{Design}} ({{DSbD}}) {{Initiative}}},
    url         = {https://www.cl.cam.ac.uk/research/security/ctsrd/cheri/dsbd.html}
}

@inproceedings{cheri2014,
    title       = {{The {CHERI} Capability Model: Revisiting {RISC} in an Age of Risk}},
    booktitle   = {2014 {ACM}/{IEEE} 41st International Symposium on Computer Architecture ({ISCA})},
    author      = {Jonathan Woodruff and Robert N. M. Watson and David Chisnall and Simon W. Moore and Jonathan Anderson and Brooks Davis and Ben Laurie and Peter G.~Neumann and Robert Norton and Michael Roe},
    year        = {2014},
    month       = {June},
    pages       = {457--468},
    publisher   = {IEEE}
}

@techreport{watson_laurie_richardson_2021, 
    url         = {https://www.capabilitieslimited.co.uk/pdfs/20210917-capltd-cheri-desktop-report-version1-FINAL.pdf}, 
    title       = {{Assessing the Viability of an Open- Source CHERI Desktop Software Ecosystem}}, 
    institution = {Capabilities Limited}, 
    author      = {Watson, Robert and Laurie, Ben and Richardson, Alex}, 
    year        = {2021}, 
    month       = {Sep}
}

@misc{miller_2019,
    author      = {Miller, Matt},
    title       = {{Trends, challenges, and strategic shifts in the software vulnerability mitigation landscape}},
    note        = {Presented at BlueHat IL},
    url         = {https://msrnd-cdn-stor.azureedge.net/bluehat/bluehatil/2019/assets/doc/Trends%2C%20Challenges%2C%20and%20Strategic%20Shifts%20in%20the%20Software%20Vulnerability%20Mitigation%20Landscape.pdf},
    month       = {Feb},
    year        = {2019}
}

@misc{richardson_2022,
    author      = {Richardson, Alex},
    title       = {{Porting C/C++ software to Morello}},
    note        = {Presented at CHERI Technical Workshop 2022},
    url         = {https://soft-dev.org/events/cheritech22/slides/Richardson.pdf},
    month       = {Sep},
    year        = {2022}
}

@misc{chisnall_2022,
    author      = {Chisnall, David},
    title       = {{Towards a Safe, High-Performance Heap Allocator}},
    note        = {Presented at CHERI Technical Workshop 2022},
    url         = {https://soft-dev.org/events/cheritech22/slides/Chisnall.pdf},
    month       = {Sep},
    year        = {2022}
}

@inproceedings{watson_2015,
    author      = {Watson, Robert N.M. and Woodruff, Jonathan and Neumann, Peter G. and Moore, Simon W. and Anderson, Jonathan and Chisnall, David and Dave, Nirav and Davis, Brooks and Gudka, Khilan and Laurie, Ben and Murdoch, Steven J. and Norton, Robert and Roe, Michael and Son, Stacey and Vadera, Munraj},
    booktitle     = {{2015 IEEE Symposium on Security and Privacy}}, 
    title         = {{CHERI: A Hybrid Capability-System Architecture for Scalable Software Compartmentalization}}, 
    year          = {2015},
    pages         = {20-37},
    issn          = {1081-6011},
    doi           = {10.1109/SP.2015.9}
}

@article{peta_1970, 
    title       = {{C Programming Language Still Ruling the World}}, 
    volume      = {22}, 
    issn        = {0975-4172},
    number      = {1}, 
    journal     = {Global Journal of Computer Science and Technology}, 
    author      = {Saphalya Peta}, 
    year        = {1970}, 
    month       = {Jan},
    pages       = {1–5} 
}

@article{chisnall_2015,
    author      = {Chisnall, David and Rothwell, Colin and Watson, Robert N.M. and Woodruff, Jonathan and Vadera, Munraj and Moore, Simon W. and Roe, Michael and Davis, Brooks and Neumann, Peter G.},
    title       = {{Beyond the PDP-11: Architectural Support for a Memory-Safe C Abstract Machine}},
    year        = {2015},
    issue_date  = {April 2015},
    publisher   = {Association for Computing Machinery},
    address     = {New York, NY, USA},
    volume      = {50},
    number      = {4},
    issn        = {0362-1340},
    journal     = {SIGPLAN Not.},
    month       = {Mar},
    pages       = {117–130},
    numpages    = {14},
    keywords    = {processor design, security, C language, bounds checking, capabilities, compilers, memory protection, memory safety}
}

@techreport{watson_et_al_2020,
    address     = {Cambridge, England}, 
    title       = {{Capability Hardware Enhanced RISC Instructions: CHERI Instruction-Set Architecture (Version 8)}},
    institution = {University of Cambridge}, 
    author      = {Watson, Robert N. M. and Neumann, Peter G. and Woodruff, Jonathan and Roe, Michael and Almatary, Hesham and Anderson, Jonathan and Baldwin, John and Barnes, Graeme and Chisnall, David and Clarke, Jessica and et al.},
    issn        = {1476-2986},
    url         = {https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-951.pdf},
    month       = {Oct},
    year        = {2020}
} 

@article{woodruff_2019,
    author      = {Woodruff, Jonathan and Joannou, Alexandre and Xia, Hongyan and Fox, Anthony and Norton, Robert M. and Chisnall, David and Davis, Brooks and Gudka, Khilan and Filardo, Nathaniel W. and Markettos, A. Theodore and Roe, Michael and Neumann, Peter G. and Watson, Robert N. M. and Moore, Simon W.},
    journal     = {IEEE Transactions on Computers}, 
    title       = {{CHERI Concentrate: Practical Compressed Capabilities}}, 
    year        = {2019},
    volume      = {68},
    number      = {10},
    pages       = {1455-1469},
    doi         = {10.1109/TC.2019.2914037}
}

@techreport{watson_cc_2019,
    author      = {Watson, Robert N. M. and Richardson, Alexander and Davis, Brooks and Baldwin, John and Chisnall, David and Clarke, Jessica and Filardo, Nathaniel and Moore, Simon M. and Napierala, Edward and Sewell, Peter and Neumann, Peter G.},
    title       = {{CHERI C/C++ Programming Guide}},
    institution = {University of Cambridge},
    address     = {Cambridge, England},
    issn        = {1476-2986},
    url         = {https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-947.pdf},
    month       = {Jun},
    year        = {2020}
}

@inproceedings{filardo_2020,
    author      = {Wesley Filardo, Nathaniel and Gutstein, Brett F. and Woodruff, Jonathan and Ainsworth, Sam and Paul-Trifu, Lucian and Davis, Brooks and Xia, Hongyan and Tomasz Napierala, Edward and Richardson, Alexander and Baldwin, John and Chisnall, David and Clarke, Jessica and Gudka, Khilan and Joannou, Alexandre and Theodore Markettos, A. and Mazzinghi, Alfredo and Norton, Robert M. and Roe, Michael and Sewell, Peter and Son, Stacey and Jones, Timothy M. and Moore, Simon W. and Neumann, Peter G. and Watson, Robert N. M.},
    booktitle   = {2020 IEEE Symposium on Security and Privacy (SP)}, 
    title       = {{Cornucopia: Temporal Safety for CHERI Heaps}}, 
    year        = {2020},
    pages       = {608-625},
    doi         = {10.1109/SP40000.2020.00098}
}

@techreport{mte_2021,
    title       = {{Armv8.5-A Memory Tagging Extension}},
    url         = {https://documentation-service.arm.com/static/624ea580caabfd7b3c13e23f?token=},
    month       = {Jun},
    year        = {2021}
}

@inproceedings{brausse_2022,
    author      = {Brau\ss{}e, Franz and Shmarov, Fedor and Menezes, Rafael and Gadelha, Mikhail R. and Korovin, Konstantin and Reger, Giles and Cordeiro, Lucas C.},
    title       = {{ESBMC-CHERI: Towards Verification of C Programs for CHERI Platforms with ESBMC}},
    year        = {2022},
    isbn        = {9781450393799},
    publisher   = {Association for Computing Machinery},
    address     = {New York, NY, USA},
    booktitle   = {Proceedings of the 31st ACM SIGSOFT International Symposium on Software Testing and Analysis},
    pages       = {773–776},
    numpages    = {4},
    keywords    = {bounded model checking, CHERI, capability hardware, formal methods, ARM Morello},
    location    = {Virtual, South Korea},
    series      = {ISSTA 2022}
}

@inproceedings{fragoso_2020,
    author      = {Fragoso Santos, Jos\'{e} and Maksimovi\'{c}, Petar and Ayoun, Sacha-\'{E}lie and Gardner, Philippa},
    title       = {{Gillian, Part i: A Multi-Language Platform for Symbolic Execution}},
    year        = {2020},
    isbn        = {9781450376136},
    publisher   = {Association for Computing Machinery},
    address     = {New York, NY, USA},
    booktitle   = {Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation},
    pages       = {927–942},
    numpages    = {16},
    keywords    = {parametric semantics, bug-finding, bounded verification, Symbolic execution, C, JavaScript},
    location    = {London, UK},
    series      = {PLDI 2020}
}

@book{nipkow_2002,
    author      = {Nipkow, Tobias and Paulson, Lawrence C. and Wenzel, Markus},
    doi         = {10.1007/3-540-45949-9},
    issn        = {0302-9743},
    isbn        = {3-540-43376-7},
    publisher   = {Springer},
    series      = {[ecture Notes in Computer Science},
    title       = {{Isabelle/HOL - A Proof Assistant for Higher-Order Logic}},
    year        = {2002}
}

@manual{morello_2022,
    title       = {{Arm Architecture Reference Manual Supplement Morello for A-Profile Architecture}},
    organization= {ARM Ltd.},
    year        = {2022},
    url         = {https://documentation-service.arm.com/static/61e577e1b691546d37bd38a0?token=},
    version     = {A.k},
    numpages    = {1294},
    
}

@inproceedings{maksimovic_2021,
    author      = {Maksimovic, Petar and Ayoun, Sacha-Elie and Santos, Jose Fragoso and Gardner, Philippa},
    editor      = {Silva, Alexandra and Leino, K. Rustan M.},
    title       = {Gillian, Part {II:} Real-World Verification for JavaScript and {C}},
    booktitle   = {{Proceedings of the 33\textsuperscript{rd} Computer Aided Verification International Conference, {CAV} 2021, Virtual Event, July 20-23, 2021, Part {II}}},
    series      = {Lecture Notes in Computer Science},
    volume      = {12760},
    pages       = {827--850},
    publisher   = {Springer},
    year        = {2021},
    doi         = {10.1007/978-3-030-81688-9\_38}
}

@misc{gillian_2021,
    doi         = {10.48550/ARXIV.2105.14769},
    url         = {https://arxiv.org/abs/2105.14769},
    author      = {Maksimovic, Petar and Santos, Jose Fragoso and Ayoun, Sacha-Elie and Gardner, Philippa},
    keywords    = {Programming Languages (cs.PL), Logic in Computer Science (cs.LO), FOS: Computer and information sciences, FOS: Computer and information sciences},
    title       = {{Gillian: A Multi-Language Platform for Unified Symbolic Analysis}},
    publisher   = {arXiv},
    year        = {2021},
    copyright   = {Creative Commons Attribution 4.0 International}
}

@article{old_gillian_2020,
    author      = {Jose Fragoso Santos and Petar Maksimovic and Sacha-Elie Ayoun and Philippa Gardner},
    title       = {{Gillian: Compositional Symbolic Execution for All}},
    journal     = {CoRR},
    volume      = {abs/2001.05059},
    year        = {2020},
    url         = {https://arxiv.org/abs/2001.05059},
    eprinttype  = {arXiv},
    eprint      = {2001.05059},
    timestamp   = {Sat, 23 Jan 2021 01:19:30 +0100},
    biburl      = {https://dblp.org/rec/journals/corr/abs-2001-05059.bib},
    bibsource   = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{calcagno_2007,
    author      = {Calcagno, Cristiano and O'Hearn, Peter W. and Yang, Hongseok},
    booktitle   = {22nd Annual IEEE Symposium on Logic in Computer Science (LICS 2007)}, 
    title       = {{Local Action and Abstract Separation Logic}}, 
    year        = {2007},
    pages       = {366-378}
}

@techreport{leroy_2012,
  title         = {{The CompCert Memory Model, Version 2}},
  author        = {Leroy, Xavier and Appel, Andrew W. and Blazy, Sandrine and Stewart, Gordon},
  type          = {Research Report},
  number        = {RR-7987},
  pages         = {26},
  institution   = {{INRIA}},
  year          = {2012},
  month         = {Jun},
  keywords      = {Memory models ; formal semantics ; verified compilation ; CompCert},
  pdf           = {https://hal.inria.fr/hal-00703441/file/RR-7987.pdf},
}

@article{armstrong_2019,
    author      = {Armstrong, Alasdair and Bauereiss, Thomas and Campbell, Brian and Reid, Alastair and Gray, Kathryn E. and Norton, Robert M. and Mundkur, Prashanth and Wassell, Mark and French, Jon and Pulte, Christopher and Flur, Shaked and Stark, Ian and Krishnaswami, Neel and Sewell, Peter},
    title       = {{ISA Semantics for ARMv8-a, RISC-v, and CHERI-MIPS}},
    year        = {2019},
    issue_date  = {January 2019},
    publisher   = {Association for Computing Machinery},
    address     = {New York, NY, USA},
    volume      = {3},
    number      = {POPL},
    journal     = {Proc. ACM Program. Lang.},
    month       = {jan},
    articleno   = {71},
    numpages    = {31},
    keywords    = {Instruction Set Architectures, Semantics, Theorem Proving}
}

@online{cheri_mips_github,
    title       = {{Sail model of CHERI-MIPS ISA}},
    publisher   = {Github},
    journal     = {Github Repository},
    howpublished= {\url{https://github.com/CTSRD-CHERI/sail-cheri-mips}}
}

@online{cheri_morello_github,
    title       = {{Morello Sail specification}},
    publisher   = {Github},
    journal     = {Github Repository},
    howpublished= {\url{https://github.com/CTSRD-CHERI/sail-morello}}
}

@online{cheri_riscv_github,
    title       = {{CHERI RISC-V Sail model}},
    publisher   = {Github},
    journal     = {Github Repository},
    howpublished= {\url{https://github.com/CTSRD-CHERI/sail-cheri-riscv}}
}

@online{cheri_compressed_cap,
    title       = {{cheri-compressed-cap}},
    publisher   = {Github},
    journal     = {Github Repository},
    howpublished= {\url{https://github.com/CTSRD-CHERI/cheri-compressed-cap}}
}

@online{cheri_c_tests,
    title       = {{CHERI C Tests}},
    publisher   = {Github},
    journal     = {Github Repository},
    howpublished= {\url{https://github.com/CTSRD-CHERI/cheri-c-tests}}
}

@inproceedings{klein_2012,
    author      = {Klein, Gerwin and Kolanski, Rafal and Boyton, Andrew},
    editor      = {Beringer, Lennart and Felty, Amy},
    title       = {{Mechanised Separation Algebra}},
    booktitle   = {Interactive Theorem Proving},
    year        = {2012},
    publisher   = {Springer Berlin Heidelberg},
    address     = {Berlin, Heidelberg},
    pages       = {332--337},
    isbn        = {978-3-642-32347-8},
    doi         = {10.1007/978-3-642-32347-8_22}
}

@inproceedings{haftmann_2013,
    author      = {Haftmann, Florian and Krauss, Alexander and Kun{\v{c}}ar, Ond{\v{r}}ej and Nipkow, Tobias},
    editor      = {Blazy, Sandrine and Paulin-Mohring, Christine and Pichardie, David},
    title       = {{Data Refinement in Isabelle/HOL}},
    booktitle   = {Interactive Theorem Proving},
    year        = {2013},
    publisher   = {Springer Berlin Heidelberg},
    address     = {Berlin, Heidelberg},
    pages       = {100--115},
    isbn        = {978-3-642-39634-2},
    doi         = {10.1007/978-3-642-39634-2_10}
}

@inproceedings{lochbihler_2013,
    author      = {Lochbihler, Andreas},
    editor      = {Blazy, Sandrine and Paulin-Mohring, Christine and Pichardie, David},
    title       = {{Light-Weight Containers for Isabelle: Efficient, Extensible, Nestable}},
    booktitle   = {Interactive Theorem Proving},
    year        = {2013},
    publisher   = {Springer Berlin Heidelberg},
    address     = {Berlin, Heidelberg},
    pages       = {116--132},
    isbn        = {978-3-642-39634-2},
    doi         = {10.1007/978-3-642-39634-2_11}
}

@article{haftmann_2021,
    author      = {Haftmann, Florian},
    month       = {Dec},
    year        = {2021},
    url         = {https://isabelle.in.tum.de/doc/codegen.pdf},
    title       = {{Code generation from Isabelle/HOL theories}}
}

@article{memarian_2019,
    author      = {Memarian, Kayvan and Gomes, Victor B. F. and Davis, Brooks and Kell, Stephen and Richardson, Alexander and Watson, Robert N. M. and Sewell, Peter},
    title       = {{Exploring C Semantics and Pointer Provenance}},
    year        = {2019},
    issue_date  = {January 2019},
    publisher   = {Association for Computing Machinery},
    address     = {New York, NY, USA},
    volume      = {3},
    number      = {POPL},
    journal     = {Proc. ACM Program. Lang.},
    month       = {jan},
    articleno   = {67},
    numpages    = {32},
    keywords    = {C}
}

@article{ohearn_2019,
    author      = {O'Hearn, Peter W.},
    title       = {Incorrectness Logic},
    year        = {2019},
    issue_date  = {January 2020},
    publisher   = {Association for Computing Machinery},
    address     = {New York, NY, USA},
    volume      = {4},
    number      = {POPL},
    url         = {https://doi.org/10.1145/3371078},
    doi         = {10.1145/3371078},
    journal     = {Proc. ACM Program. Lang.},
    month       = {dec},
    articleno   = {10},
    numpages    = {32},
    keywords    = {none}
}

@article{beeren_2016,
    author      = {Joel Beeren and Matthew Fernandez and Xin Gao and Gerwin Klein and Rafal Kolanski and Japheth Lim and Corey Lewis and Daniel Matichuk and Thomas Sewell},
    title       = {{Finite Machine Word Library}},
    journal     = {Archive of Formal Proofs},
    month       = {June},
    year        = {2016},
    note        = {\url{https://isa-afp.org/entries/Word_Lib.html}, Formal proof development},
    ISSN        = {2150-914x},
}

@article{krebbers_2016,
    author      = {Krebbers, Robbert},
    title       = {{A Formal C Memory Model for Separation Logic}},
    journal     = {Journal of Automated Reasoning},
    year        = {2016},
    month       = {Dec},
    day         = {01},
    volume      = {57},
    number      = {4},
    pages       = {319-387},
    issn        = {1573-0670},
    doi         = {10.1007/s10817-016-9369-1},
}

@article{tuch_2009,
    author      = {Tuch, Harvey},
    title       = {{Formal Verification of C Systems Code}},
    journal     = {Journal of Automated Reasoning},
    year        = {2009},
    month       = {Apr},
    day         = {01},
    volume      = {42},
    number      = {2},
    pages       = {125-187},
    issn        = {1573-0670},
    doi         = {10.1007/s10817-009-9120-2},
}

@article{cohen_2009,
    title       = {{A Precise Yet Efficient Memory Model For C}},
    journal     = {Electronic Notes in Theoretical Computer Science},
    volume      = {254},
    pages       = {85-103},
    year        = {2009},
    note        = {Proceedings of the 4th International Workshop on Systems Software Verification (SSV 2009)},
    issn        = {1571-0661},
    doi         = {https://doi.org/10.1016/j.entcs.2009.09.061},
    author      = {Ernie Cohen and Michał Moskal and Stephan Tobies and Wolfram Schulte},
    keywords    = {deductive program verification, C programming language, memory models},
}

@InProceedings{krebbers_2014,
    author      = {Krebbers, Robbert and Leroy, Xavier and Wiedijk, Freek},
    editor      = {Klein, Gerwin and Gamboa, Ruben},
    title       = {{Formal C Semantics: CompCert and the C Standard}},
    booktitle   = {Interactive Theorem Proving},
    year        = {2014},
    publisher   = {Springer International Publishing},
    address     = {Cham},
    pages       = {543--548},
    isbn        = {978-3-319-08970-6}
}

@misc{park_2022,
    doi         = {10.48550/arxiv.2211.07511},
    url         = {https://arxiv.org/abs/2211.07511},
    author      = {Park, Seung Hoon and Pai, Rekha and Melham, Tom},
    title       = {{A Formal CHERI-C Semantics for Verification}},
    publisher   = {arXiv},
    year        = {2022},
    note        = {Submitted to TACAS 2023},
}

@book{cstandard_2003,
    title       = {{The C Standard: Incorporating Technical Corrigendum 1}},
    author      = {British Standards Institution and BSI (The British Standards Institution)},
    isbn        = {9780470846742},
    year        = {2003},
    publisher   = {Wiley}
}
