I am a researcher in the Laboratory for Foundations of Computer Science, part of the School of Informatics at the University of Edinburgh.
I currently work on specifications of instruction set architectures and tools for working with them. This is supported by the Digital Security by Design challenge which is exploring industrial strength application of the ideas from the CHERI project; and the Rigorous Engineering for Mainstream Systems (REMS) project, in particular our Sail specification language.
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 ]
As a member of the EU CerCo project, I worked on the formal verification of the front end of a compiler which lifted cost information from a machine code analysis to the input C source code. A summary of our work can be found in the FOPARA 2013 post-proceedings.
Roberto M. Amadio, Nicolas Ayache, Francois Bobot, Jaap P. Boender, Brian Campbell, Ilias Garnier, Antoine Madet, James McKinna, Dominic P. Mulligan, Mauro Piccolo, Randy Pollack, Yann Régis-Gianas, Claudio Sacerdoti Coen, Ian Stark, and Paolo Tranquilli. Certified complexity (CerCo). In Ugo Dal Lago and Ricardo Peña, editors, Foundational and Practical Aspects of Resource Analysis (FOPARA 2013), volume 8552 of Lecture Notes in Computer Science, pages 1--18. Springer, 2014. The final publication is available at link.springer.com. [ bib | DOI | Author's version ]
During CerCo, I wrote an executable semantics for the CompCert C language, which enabled testing of CompCert's specification against test suites of C code.
Brian Campbell. An executable semantics for CompCert C. In Chris Hawblitzel and Dale Miller, editors, The Second International Conference on Certified Programs and Proofs (CPP 2012), volume 7679 of Lecture Notes in Computer Science, pages 60--75. Springer-Verlag, 2012. The original publication is available at www.springerlink.com. [ bib | DOI | Author's version | slides ]
In the ReQueST project I worked on formally verifying a proof checker for a simple resource checking logic over Java bytecode.
During my PhD I studied static prediction of stack-space requirements for functional programs alongside the MRG project using a type-based static analysis. The best document describing my PhD work is my thesis: Type-based amortized stack memory prediction. Papers covering most of this work appeared at TFP 2008), and space bounds with respect to the depth of data structures was presented at ESOP'09.
Brian Campbell. Prediction of linear memory usage for first-order functional programs. In Peter Achten, Pieter Koopman, and Marco T. Morazán, editors, Trends in Functional Programming, volume 9, pages 1--16. Intellect, 2009. [ bib | slides ]
Brian Campbell. Amortised memory analysis using the depth of data structures. In Giuseppe Castagna, editor, Programming Languages and Systems: 18th European Symposium on Programming (ESOP 2009), volume 5502 of Lecture Notes in Computer Science, pages 190--204. Springer-Verlag, 2009. Copyright Springer-Verlag Berlin Heidelberg 2009. [ bib | DOI | Author's version | slides ]
Brian Campbell. Type-based amortized stack memory prediction. PhD thesis, University of Edinburgh, 2008. [ bib | .pdf ]
I was one of the organisers for the March 2011 Scottish Programming Languages Seminar meeting.
My photographs from the 2005 Marktoberdorf Summer School are online too, plus a small physics demo from our excursion (you will need to rotate your head, because my camera is not smart enough to rotate the video, and I'm too lazy).
Last modified Monday, 18-May-2020 15:48:35 BST.