Follow
Brian Campbell
Brian Campbell
Laboratory for Foundations of Computer Science, University of Edinburgh
Verified email at ed.ac.uk - Homepage
Title
Cited by
Cited by
Year
ISA semantics for ARMv8-A, RISC-V, and CHERI-MIPS
A Armstrong, T Bauereiss, B Campbell, A Reid, KE Gray, RM Norton, ...
Proceedings of the ACM on Programming Languages 3 (POPL), 71, 2019
1752019
Rigorous engineering for hardware security: Formal modelling and proof in the CHERI design and implementation process
K Nienhuis, A Joannou, T Bauereiss, A Fox, M Roe, B Campbell, M Naylor, ...
2020 IEEE Symposium on Security and Privacy (SP), 1003-1020, 2020
592020
Certified complexity (CerCo)
RM Amadio, N Ayache, F Bobot, JP Boender, B Campbell, I Garnier, ...
International Workshop on Foundational and Practical Aspects of Resource …, 2013
502013
Randomised testing of a microprocessor model using SMT-solver state generation
B Campbell, I Stark
Science of Computer Programming 118, 60-76, 2016
432016
Amortised Memory Analysis using the Depth of Data Structures.
B Campbell
ESOP 5502, 190-204, 2009
432009
Verified security for the Morello capability-enhanced prototype Arm architecture
T Bauereiss, B Campbell, T Sewell, A Armstrong, L Esswood, I Stark, ...
University of Cambridge, Computer Laboratory, 2021
332021
Islaris: verification of machine code against authoritative ISA semantics
M Sammler, A Hammond, R Lepigre, B Campbell, J Pichon-Pharabod, ...
Proceedings of the 43rd ACM SIGPLAN International Conference on Programming …, 2022
262022
Isla: Integrating full-scale ISA semantics and axiomatic concurrency models
A Armstrong, B Campbell, B Simner, C Pulte, P Sewell
Computer Aided Verification: 33rd International Conference, CAV 2021 …, 2021
252021
An executable semantics for Compcert C
B Campbell
International Conference on Certified Programs and Proofs, 60-75, 2012
222012
Type-based amortized stack memory prediction
B Campbell
The University of Edinburgh, 2008
172008
Extracting Behaviour from an Executable Instruction Set Model
B Campbell, I Stark
Formal Methods in Computer-Aided Design, 2016
132016
Detailed models of instruction set architectures: From pseudocode to formal semantics
A Armstrong, T Bauereiss, B Campbell, S Flur, KE Gray, P Mundkur, ...
Proceedings of the 25th Automated Reasoning Workshop: Bridging the Gap …, 2018
122018
Certified complexity
R Armadio, A Asperti, N Ayache, B Campbell, D Mulligan, R Pollack, ...
Procedia Computer Science 7, 175-177, 2011
102011
Fast and Correct Load-Link/Store-Conditional Instruction Handling in DBT Systems
M Kristien, T Spink, B Campbell, S Sarkar, I Stark, B Franke, I Böhm, ...
IEEE Transactions on Computer-Aided Design of Integrated Circuits and …, 2020
92020
Prediction of linear memory usage for first-order functional programs.
B Campbell
Trends in Functional Programming 9, 1-16, 2008
92008
Isla: Integrating full-scale ISA semantics and axiomatic concurrency models (extended version)
A Armstrong, B Campbell, B Simner, C Pulte, P Sewell
Extended version of a paper in Proceedings of CAV, 2021
42021
Formal Mechanised Semantics of CHERI C: Capabilities, Provenance, and Undefined Behaviour
V Zaliva, K Memarian, RDO Almeida, J Clarke, B Davis, A Richardson, ...
29th ACM International Conference on Architectural Support for Programming …, 2023
32023
The Sail instruction-set semantics specification language
A Armstrong, T Bauereiss, B Campbell, KE Gray, R Norton-Wright, C Pulte, ...
32021
CHERI C semantics as an extension of the ISO C17 standard
V Zaliva, K Memarian, R Almeida, J Clarke, B Davis, A Richardson, ...
University of Cambridge, Computer Laboratory, 2023
12023
Foreword Preface
M Hofmann, D Aspinall, B Campbell, I Stark, P Stevens
THEORETICAL COMPUTER SCIENCE 741, 1-2, 2018
2018
The system can't perform the operation now. Try again later.
Articles 1–20