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