Prediction of linear memory usage for first-order functional programs. - Brian Campbell 001 (Trends in Functional Programming, 2008)

Type-based amortized stack memory prediction. - Brian Campbell 001 (2008)

Amortised Memory Analysis Using the Depth of Data Structures. - Brian Campbell 001 (ESOP, 2009)

Certified Complexity. - R. Armadio; Andrea Asperti; Nicholas Ayache; Brian Campbell 001; Dominic P. Mulligan; Randy Pollack; Yann Régis-Gianas; Claudio Sacerdoti Coen; Ian Stark (FET, 2011)

An Executable Semantics for CompCert C. - Brian Campbell 001 (CPP, 2012)

Certified Complexity (CerCo). - Roberto M. Amadio; Nicholas Ayache; François Bobot; Jaap Boender; Brian Campbell 001; Ilias Garnier; Antoine Madet; James McKinna; Dominic P. Mulligan; Mauro Piccolo; Randy Pollack; Yann Régis-Gianas; et al. (FOPARA, 2013)

Extracting behaviour from an executable instruction set model. - Brian Campbell 001; Ian Stark (FMCAD, 2016)

Randomised testing of a microprocessor model using SMT-solver state generation. - Brian Campbell 001; Ian Stark (Sci. Comput. Program., 2016)

Foreword. - Martin Hofmann 001; David Aspinall 001; Brian Campbell 001; Ian Stark; Perdita Stevens (Theor. Comput. Sci., 2018)

ISA semantics for ARMv8-a, RISC-v, and CHERI-MIPS. - Alasdair Armstrong; Thomas Bauereiss; Brian Campbell 001; Alastair Reid 001; Kathryn E. Gray; Robert M. Norton; Prashanth Mundkur; Mark Wassell; Jon French; Christopher Pulte; Shaked Flur; Ian Stark; et al. (Proc. ACM Program. Lang., 2019)

Rigorous engineering for hardware security: Formal modelling and proof in the CHERI design and implementation process. - Kyndylan Nienhuis; Alexandre Joannou; Thomas Bauereiss; Anthony C. J. Fox; Michael Roe; Brian Campbell 001; Matthew Naylor; Robert M. Norton; Simon W. Moore; Peter G. Neumann; Ian Stark; Robert N. M. Watson; et al. (SP, 2020)

Fast and Correct Load-Link/Store-Conditional Instruction Handling in DBT Systems. - Martin Kristien; Tom Spink; Brian Campbell 001; Susmit Sarkar; Ian Stark; Björn Franke; Igor Böhm; Nigel P. Topham (IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 2020)

Isla: Integrating Full-Scale ISA Semantics and Axiomatic Concurrency Models. - Alasdair Armstrong; Brian Campbell 001; Ben Simner; Christopher Pulte; Peter Sewell (CAV (1), 2021)

Verified Security for the Morello Capability-enhanced Prototype Arm Architecture. - Thomas Bauereiss; Brian Campbell 001; Thomas Sewell; Alasdair Armstrong; Lawrence Esswood; Ian Stark; Graeme Barnes; Robert N. M. Watson; Peter Sewell (ESOP, 2022)

Islaris: verification of machine code against authoritative ISA semantics. - Michael Sammler; Angus Hammond; Rodolphe Lepigre; Brian Campbell 001; Jean Pichon-Pharabod; Derek Dreyer; Deepak Garg 001; Peter Sewell (PLDI, 2022)

Formal Mechanised Semantics of CHERI C: Capabilities, Undefined Behaviour, and Provenance. - Vadim Zaliva; Kayvan Memarian; Ricardo Almeida 003; Jessica Clarke 001; Brooks Davis; Alexander Richardson 001; David Chisnall; Brian Campbell 001; Ian Stark; Robert N. M. Watson; Peter Sewell (ASPLOS (1), 2024)

Relaxed exception semantics for Arm-A (extended version). - Ben Simner; Alasdair Armstrong; Thomas Bauereiss; Brian Campbell 001; Ohad Kammar; Jean Pichon-Pharabod; Peter Sewell (CoRR, 2024)

Isla: integrating full-scale ISA semantics and axiomatic concurrency models (extended version). - Alasdair Armstrong; Brian Campbell 001; Ben Simner; Christopher Pulte; Peter Sewell (Formal Methods Syst. Des., 2024)

A CHERI C Memory Model for Verified Temporal Safety. - Vadim Zaliva; Kayvan Memarian; Brian Campbell 001; Ricardo Almeida 003; Nathaniel Wesley Filardo; Ian Stark; Peter Sewell (CPP, 2025)

Precise exceptions in relaxed architectures. - Ben Simner; Alasdair Armstrong; Thomas Bauereiss; Brian Campbell 001; Ohad Kammar; Jean Pichon-Pharabod; Peter Sewell (ISCA, 2025)

Morello-Cerise: A Proof of Strong Encapsulation for the Arm Morello Capability Hardware Architecture. - Angus Hammond; Ricardo Almeida 003; Thomas Bauereiss; Brian Campbell 001; Ian Stark; Peter Sewell (Proc. ACM Program. Lang., 2025)