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
802019
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
392013
Amortised Memory Analysis using the Depth of Data Structures.
B Campbell
ESOP 5502, 190-204, 2009
382009
Randomised testing of a microprocessor model using SMT-solver state generation
B Campbell, I Stark
Science of Computer Programming 118, 60-76, 2016
322016
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
252020
An executable semantics for Compcert C
B Campbell
International Conference on Certified Programs and Proofs, 60-75, 2012
212012
Type-based amortized stack memory prediction
B Campbell
The University of Edinburgh, 2008
162008
Certified complexity
R Armadio, A Asperti, N Ayache, B Campbell, D Mulligan, R Pollack, ...
Procedia Computer Science 7, 175-177, 2011
102011
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
82018
Extracting Behaviour from an Executable Instruction Set Model
B Campbell, I Stark
Formal Methods in Computer-Aided Design, 2016
82016
Prediction of linear memory usage for first-order functional programs.
B Campbell
Trends in Functional Programming 9, 1-16, 2008
82008
Isla: Integrating full-scale ISA semantics and axiomatic concurrency models
A Armstrong, B Campbell, B Simner, C Pulte, P Sewell
International Conference on Computer Aided Verification, 303-316, 2021
52021
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
42021
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
32020
The Sail instruction-set semantics specification language
A Armstrong, T Bauereiss, B Campbell, KE Gray, R Norton-Wright, C Pulte, ...
22021
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
12021
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–17