Brian Campbell

I am a researcher in the Laboratory for Foundations of Computer Science, part of the School of Informatics at the University of Edinburgh.

Current research

I currently work on the Rigorous Engineering for Mainstream Systems (REMS) project. Most recently I have been working on randomised testing of processor models written in the L3 language. At FMICS 2014 I presented a paper about testing a model of the ARM Cortex-M0 microcontroller core, which includes some timing properties. I also gave a talk about this at the January 2014 Scottish Theorem Provers meeting. We intend to use this model in a timing-aware decompilation experiment.

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 [ bib | DOI | Author's version | slides ]

Previous work

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 [ 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 [ 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. Type-based amortized stack memory prediction. PhD thesis, University of Edinburgh, 2008. [ bib | .pdf ]

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 ]


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).
Room 5.28, Informatics Forum.

Last modified Wednesday, 19-Nov-2014 14:18:15 GMT.