University of Edinburgh
United Kingdom of Great Britain and Northern Ireland
→
Brian Campbell
Work
Publications
Precise exceptions in relaxed architectures
conference-paper
Morello-Cerise: A Proof of Strong Encapsulation for the Arm Morello Capability Hardware Architecture
Proceedings of the ACM on Programming Languages
journal-article
A CHERI C Memory Model for Verified Temporal Safety
conference-paper
Formal Mechanised Semantics of CHERI C: Capabilities, Undefined Behaviour, and Provenance
conference-paper
Verified Security for the Morello Capability-enhanced Prototype Arm Architecture
book-chapter
Isla: Integrating full-scale ISA semantics andaxiomatic concurrency models
Proceedings of the 33rd International Conference on Computer-Aided Verification (CAV 2021)
conference-paper
Fast and Correct Load-Link/Store-Conditional Instruction Handling in DBT Systems
IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems
journal-article
Rigorous engineering for hardware security: Formal modelling and proof in the CHERI design and implementation process
2020 IEEE Symposium on Security and Privacy (SP)
conference-paper
ISA Semantics for ARMv8-A, RISC-V, and CHERI-MIPS
Proceedings of the ACM on Programming Languages
journal-article
Foreword
Theoretical Computer Science
other
Extracting Behaviour from an Executable Instruction Set Model
Proceedings of the 16th Conference on Formal Methods in Computer - Aided Design (FMCAD 2016)
conference-paper
Randomised testing of a microprocessor model using SMT-solver state generation
Science of Computer Programming
journal-article
Certified Complexity (CerCo)
Foundational and Practical Aspects of Resource Analysis
conference-paper
Randomised Testing of a Microprocessor Model Using SMT-Solver State Generation
Formal Methods for Industrial Critical Systems
conference-paper
An Executable Semantics for CompCert C
Certified Programs and Proofs
conference-paper
Certified Complexity
Procedia Computer Science
journal-article
Amortised Memory Analysis Using the Depth of Data Structures
Programming Languages and Systems
conference-paper
Prediction of linear memory usage for first-order functional programs
Proceedings of the Nineth Symposium on Trends in Functional Programming, TFP 2008, Nijmegen, The Netherlands, May 26-28, 2008.
conference-paper