Brian Campbell

23 papers A* 3A 2B 3C 1Journal 8Unranked 5
YearRankTypeTitle / Venue / Authors
2026 J jnl
ArchSem: Reusable Rigorous Semantics of Relaxed Architectures.
Proc. ACM Program. Lang.
Thibaut Pérami, Thomas Bauereiss, Brian Campbell, Zongyuan Liu, Nils Lauermann, Alasdair Armstrong, Peter Sewell
2025 B conf
A CHERI C Memory Model for Verified Temporal Safety.
CPP
Vadim Zaliva, Kayvan Memarian, Brian Campbell, Ricardo Almeida, Nathaniel Wesley Filardo, Ian Stark, Peter Sewell
2025 J jnl
Morello-Cerise: A Proof of Strong Encapsulation for the Arm Morello Capability Hardware Architecture.
Proc. ACM Program. Lang.
Angus Hammond, Ricardo Almeida, Thomas Bauereiss, Brian Campbell, Ian Stark, Peter Sewell
2025 A* conf
Precise exceptions in relaxed architectures.
ISCA
Ben Simner, Alasdair Armstrong, Thomas Bauereiss, Brian Campbell, Ohad Kammar, Jean Pichon-Pharabod, Peter Sewell
2024 — conf
Formal Mechanised Semantics of CHERI C: Capabilities, Undefined Behaviour, and Provenance.
ASPLOS (1)
Vadim Zaliva, Kayvan Memarian, Ricardo Almeida, Jessica Clarke, Brooks Davis, Alexander Richardson, David Chisnall, Brian Campbell, Ian Stark, Robert N. M. Watson, Peter Sewell
2024 J jnl
Isla: integrating full-scale ISA semantics and axiomatic concurrency models (extended version).
Formal Methods Syst. Des.
Alasdair Armstrong, Brian Campbell, Ben Simner, Christopher Pulte, Peter Sewell
2024 J jnl
Relaxed exception semantics for Arm-A (extended version).
CoRR
Ben Simner, Alasdair Armstrong, Thomas Bauereiss, Brian Campbell, Ohad Kammar, Jean Pichon-Pharabod, Peter Sewell
2022 A* conf
Islaris: verification of machine code against authoritative ISA semantics.
PLDI
Michael Sammler, Angus Hammond, Rodolphe Lepigre, Brian Campbell, Jean Pichon-Pharabod, Derek Dreyer, Deepak Garg, Peter Sewell
2022 A conf
Verified Security for the Morello Capability-enhanced Prototype Arm Architecture.
ESOP
Thomas Bauereiss, Brian Campbell, Thomas Sewell, Alasdair Armstrong, Lawrence Esswood, Ian Stark, Graeme Barnes, Robert N. M. Watson, Peter Sewell
2021 — conf
Isla: Integrating Full-Scale ISA Semantics and Axiomatic Concurrency Models.
CAV (1)
Alasdair Armstrong, Brian Campbell, Ben Simner, Christopher Pulte, Peter Sewell
2020 J jnl
Fast and Correct Load-Link/Store-Conditional Instruction Handling in DBT Systems.
IEEE Trans. Comput. Aided Des. Integr. Circuits Syst.
Martin Kristien, Tom Spink, Brian Campbell, Susmit Sarkar, Ian Stark, Björn Franke, Igor Böhm, Nigel P. Topham
2020 A* conf
Rigorous engineering for hardware security: Formal modelling and proof in the CHERI design and implementation process.
SP
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
2019 J jnl
ISA semantics for ARMv8-a, RISC-v, and CHERI-MIPS.
Proc. ACM Program. Lang.
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
2018 J jnl
Foreword.
Theor. Comput. Sci.
Martin Hofmann, David Aspinall, Brian Campbell, Ian Stark, Perdita Stevens
2016 B conf
Extracting behaviour from an executable instruction set model.
FMCAD
Brian Campbell, Ian Stark
2016 J jnl
Randomised testing of a microprocessor model using SMT-solver state generation.
Sci. Comput. Program.
Brian Campbell, Ian Stark
2014 C conf
Randomised Testing of a Microprocessor Model Using SMT-Solver State Generation.
FMICS
Brian Campbell, Ian Stark
2013 — conf
Certified Complexity (CerCo).
FOPARA
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
2012 B conf
An Executable Semantics for CompCert C.
CPP
Brian Campbell
2011 — conf
Certified Complexity.
FET
R. Armadio, Andrea Asperti, Nicholas Ayache, Brian Campbell, Dominic P. Mulligan, Randy Pollack, Yann Régis-Gianas, Claudio Sacerdoti Coen, Ian Stark
2009 A conf
Amortised Memory Analysis Using the Depth of Data Structures.
ESOP
Brian Campbell
2008 — conf
Prediction of linear memory usage for first-order functional programs.
Trends in Functional Programming
Brian Campbell
2008 — —
Type-based amortized stack memory prediction.
Brian Campbell