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 Proceedings of the 41st IEEE Symposium on Security and Privacy (SP), pages 1007--1024, May 2020. [ bib | DOI | .pdf ]

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. Proc. ACM Program. Lang., 3(POPL):71:1--71:31, 2019. [ bib | DOI ]

Brian Campbell and Ian Stark. Randomised testing of a microprocessor model using SMT-solver state generation. Science of Computer Programming, 118:60--76, March 2016. [ bib | DOI | Author's version ]

Brian Campbell and Ian Stark. Extracting behaviour from an executable instruction set model. In Ruzica Piskac and Muralidhar Talupur, editors, Formal Methods in Computer-Aided Design, (FMCAD 2016), pages 33--40, 2016. http://www.fmcad.org/FMCAD16. [ bib | DOI | Author's version | slides ]

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, Formal Methods for Industrial Critical Systems (FMICS 2014), volume 8718 of Lecture Notes in Computer Science, pages 185--199. Springer, 2014. The final publication is available at link.springer.com. [ bib | DOI | Author's version | slides ]