| 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 | 172 | 2019 |
| 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 | 58 | 2020 |
| 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 | 50 | 2013 |
| Amortised Memory Analysis using the Depth of Data Structures. B Campbell ESOP 5502, 190-204, 2009 | 43 | 2009 |
| Randomised testing of a microprocessor model using SMT-solver state generation B Campbell, I Stark Science of Computer Programming 118, 60-76, 2016 | 42 | 2016 |
| 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 | 33 | 2021 |
| 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 | 26 | 2022 |
| 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 | 24 | 2021 |
| An executable semantics for Compcert C B Campbell International Conference on Certified Programs and Proofs, 60-75, 2012 | 22 | 2012 |
| Type-based amortized stack memory prediction B Campbell The University of Edinburgh, 2008 | 17 | 2008 |
| Extracting Behaviour from an Executable Instruction Set Model B Campbell, I Stark Formal Methods in Computer-Aided Design, 2016 | 13 | 2016 |
| 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 | 11 | 2018 |
| Certified complexity R Armadio, A Asperti, N Ayache, B Campbell, D Mulligan, R Pollack, ... Procedia Computer Science 7, 175-177, 2011 | 10 | 2011 |
| 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 | 9 | 2020 |
| Prediction of linear memory usage for first-order functional programs. B Campbell Trends in Functional Programming 9, 1-16, 2008 | 9 | 2008 |
| 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 | 4 | 2021 |
| 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 | 3 | 2023 |
| The Sail instruction-set semantics specification language A Armstrong, T Bauereiss, B Campbell, KE Gray, R Norton-Wright, C Pulte, ... | 3 | 2021 |
| 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 | 1 | 2023 |
| Foreword Preface M Hofmann, D Aspinall, B Campbell, I Stark, P Stevens THEORETICAL COMPUTER SCIENCE 741, 1-2, 2018 | | 2018 |
