关注
Brian Campbell
Brian Campbell
Laboratory for Foundations of Computer Science, University of Edinburgh
在 ed.ac.uk 的电子邮件经过验证 - 首页
标题
引用次数
引用次数
年份
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
1532019
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
542020
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
492013
Amortised Memory Analysis using the Depth of Data Structures.
B Campbell
ESOP 5502, 190-204, 2009
422009
Randomised testing of a microprocessor model using SMT-solver state generation
B Campbell, I Stark
Science of Computer Programming 118, 60-76, 2016
412016
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
292021
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
222022
An executable semantics for Compcert C
B Campbell
International Conference on Certified Programs and Proofs, 60-75, 2012
222012
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
212021
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
122016
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
112018
Certified complexity
R Armadio, A Asperti, N Ayache, B Campbell, D Mulligan, R Pollack, ...
Procedia Computer Science 7, 175-177, 2011
102011
Prediction of linear memory usage for first-order functional programs.
B Campbell
Trends in Functional Programming 9, 1-16, 2008
92008
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
72020
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
The Sail instruction-set semantics specification language
A Armstrong, T Bauereiss, B Campbell, KE Gray, R Norton-Wright, C Pulte, ...
22021
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
12023
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
系统目前无法执行此操作,请稍后再试。
文章 1–20