Brian Campbell

According to our database, Brian Campbell authored at least 21 papers between 2008 and 2025.

Collaborative distances:

• Dijkstra number of three.
• Erdős number of four.

2025

Morello-Cerise: A Proof of Strong Encapsulation for the Arm Morello Capability Hardware Architecture.

Angus Hammond, Ricardo Almeida, Thomas Bauereiss, Brian Campbell, Ian Stark, Peter Sewell

Proc. ACM Program. Lang., 2025

Precise exceptions in relaxed architectures.

Ben Simner, Alasdair Armstrong, Thomas Bauereiss, Brian Campbell, Ohad Kammar, Jean Pichon-Pharabod, Peter Sewell

Proceedings of the 52nd Annual International Symposium on Computer Architecture, 2025

A CHERI C Memory Model for Verified Temporal Safety.

Vadim Zaliva, Kayvan Memarian, Brian Campbell, Ricardo Almeida, Nathaniel Wesley Filardo, Ian Stark, Peter Sewell

Proceedings of the 14th ACM SIGPLAN International Conference on Certified Programs and Proofs, 2025

2024

Isla: integrating full-scale ISA semantics and axiomatic concurrency models (extended version).

Alasdair Armstrong, Brian Campbell, Ben Simner, Christopher Pulte, Peter Sewell

Formal Methods Syst. Des., October, 2024

Relaxed exception semantics for Arm-A (extended version).

Ben Simner, Alasdair Armstrong, Thomas Bauereiss, Brian Campbell, Ohad Kammar, Jean Pichon-Pharabod, Peter Sewell

CoRR, 2024

Formal Mechanised Semantics of CHERI C: Capabilities, Undefined Behaviour, and Provenance.

Vadim Zaliva, Kayvan Memarian, Ricardo Almeida, Jessica Clarke, Brooks Davis, Alexander Richardson, David Chisnall, Brian Campbell, Ian Stark, Robert N. M. Watson, Peter Sewell

Proceedings of the 29th ACM International Conference on Architectural Support for Programming Languages and Operating Systems, 2024

2022

Islaris: verification of machine code against authoritative ISA semantics.

Michael Sammler, Angus Hammond, Rodolphe Lepigre, Brian Campbell, Jean Pichon-Pharabod, Derek Dreyer, Deepak Garg, Peter Sewell

Proceedings of the PLDI '22: 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation, San Diego, CA, USA, June 13, 2022

Verified Security for the Morello Capability-enhanced Prototype Arm Architecture.

Thomas Bauereiss, Brian Campbell, Thomas Sewell, Alasdair Armstrong, Lawrence Esswood, Ian Stark, Graeme Barnes, Robert N. M. Watson, Peter Sewell

Proceedings of the Programming Languages and Systems, 2022

2021

Isla: Integrating Full-Scale ISA Semantics and Axiomatic Concurrency Models.

Alasdair Armstrong, Brian Campbell, Ben Simner, Christopher Pulte, Peter Sewell

Proceedings of the Computer Aided Verification - 33rd International Conference, 2021

2020

Fast and Correct Load-Link/Store-Conditional Instruction Handling in DBT Systems.

Martin Kristien, Tom Spink, Brian Campbell, Susmit Sarkar, Ian Stark, Björn Franke, Igor Böhm, Nigel P. Topham

IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 2020

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, Matthew Naylor, Robert M. Norton, Simon W. Moore, Peter G. Neumann, Ian Stark, Robert N. M. Watson, Peter Sewell

Proceedings of the 2020 IEEE Symposium on Security and Privacy, 2020

2019

ISA semantics for ARMv8-a, RISC-v, and CHERI-MIPS.

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, Peter Sewell

Proc. ACM Program. Lang., 2019

2018

Foreword.

Martin Hofmann, David Aspinall, Brian Campbell, Ian Stark, Perdita Stevens

Theor. Comput. Sci., 2018

2016

Extracting behaviour from an executable instruction set model.

Brian Campbell, Ian Stark

Proceedings of the 2016 Formal Methods in Computer-Aided Design, 2016

2014

Randomised Testing of a Microprocessor Model Using SMT-Solver State Generation.

Brian Campbell, Ian Stark

Proceedings of the Formal Methods for Industrial Critical Systems, 2014

2013

Certified Complexity (CerCo).

Roberto M. Amadio, Nicholas Ayache, François Bobot, Jaap 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, Paolo Tranquilli

Proceedings of the Foundational and Practical Aspects of Resource Analysis, 2013

2012

An Executable Semantics for CompCert C.

Brian Campbell

Proceedings of the Certified Programs and Proofs - Second International Conference, 2012

2011

Certified Complexity.

R. Armadio, Andrea Asperti, Nicholas Ayache, Brian Campbell, Dominic P. Mulligan, Randy Pollack, Yann Régis-Gianas, Claudio Sacerdoti Coen, Ian Stark

Proceedings of the 2nd European Future Technologies Conference and Exhibition, 2011

2009

Amortised Memory Analysis Using the Depth of Data Structures.

Brian Campbell

Proceedings of the Programming Languages and Systems, 2009

2008

Type-based amortized stack memory prediction.

Brian Campbell

PhD thesis, 2008

Prediction of linear memory usage for first-order functional programs.

Brian Campbell

Proceedings of the Nineth Symposium on Trends in Functional Programming, 2008