Filter
Conference contribution

Search results

  • 2023

    Formal Mechanised Semantics of CHERI C: Capabilities, Provenance, and Undefined Behaviour

    Zaliva, V., Memarian, K., De Oliveira Almeida, R., Clarke, J., Davis, B., Richardson, A., Chisnall, D., Campbell, B., Stark, I., Watson, R. N. M. & Sewell, P., 19 Sept 2023, (Accepted/In press) ASPLOS 2024: Proceedings of the 29th ACM International Conference on Architectural Support for Programming Languages and Operating Systems. ACM, p. 1-16 16 p.

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

    Open Access
    File
  • 2022

    Islaris: Verification of Machine Code Against Authoritative ISA Semantics

    Sammler, M., Hammond, A., Lepigre, R., Campbell, B., Pichon-Pharabod, J., Dreyer, D., Garg, D. & Sewell, P., 9 Jun 2022, Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation. Jhala, R. & Dillig, I. (eds.). ACM, p. 825-840 16 p.

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

    Open Access
    File
  • Verified Security for the Morello Capability-enhanced Prototype Arm Architecture

    Bauereiss, T., Campbell, B., Sewell, T., Armstrong, A., Esswood, L., Stark, I., Barnes, G., Watson, R. N. M. & Sewell, P., 29 Mar 2022, Programming Languages and Systems - 31st European Symposium on Programming, ESOP 2022, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Munich, Germany, April 2–7, 2022, Proceedings. Sergey, I. (ed.). Springer, p. 174-203 30 p. (Lecture Notes in Computer Science; vol. 13240).

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

    Open Access
    File
  • 2021

    Isla: Integrating full-scale ISA semantics andaxiomatic concurrency models

    Armstrong, A., Campbell, B., Simner, B., Pulte, C. & Sewell, P., 15 Jul 2021, Proceedings of the 33rd International Conference on Computer-Aided Verification (CAV 2021). Springer, p. 303-316 14 p. (Lecture Notes in Computer Science; vol. 12759).

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

    Open Access
    File
  • 2020

    Rigorous engineering for hardware security: Formal modelling and proof in the CHERI design and implementation process

    Nienhuis, K., Joannou, A., Bauereiss, T., Fox, A., Roe, M., Campbell, B., Naylor, M., Norton, R. M., Moore, S. W., Neumann, P. G., Stark, I., Watson, R. N. M. & Sewell, P., 30 Jul 2020, 2020 IEEE Symposium on Security and Privacy (SP). San Francisco, CA, USA: Institute of Electrical and Electronics Engineers, p. 1003-1020 18 p.

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

    Open Access
    File
  • 2017

    Extracting Behaviour from an Executable Instruction Set Model

    Campbell, B. & Stark, I., 27 Mar 2017, Proceedings of the 16th Conference on Formal Methods in Computer - Aided Design (FMCAD 2016). Mountain View, CA, USA: FMCAD Inc, p. 33-40 8 p.

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

    Open Access
    File
  • 2014

    Certified Complexity (CerCo)

    Amadio, R., Ayache, N., Bobot, F., Boender, J., Campbell, B., Garnier, I., Madet, A., McKinna, J., Mulligan, D., Piccolo, M., Pollack, R., Régis-Giannas, Y., Sacerdoti Coen, C., Stark, I. & Tranquilli, P., 2014, Foundational and Practical Aspects of Resource Analysis: Revised Selected Papers from the Third International Workshop, FOPARA 2013, Bertinoro, Italy, August 29-31, 2013. Springer, p. 1-18 18 p. (Lecture Notes in Computer Science; vol. 8552).

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

    Open Access
    File
  • Randomised Testing of a Microprocessor Model Using SMT-Solver State Generation

    Campbell, B. & Stark, I., 2014, Formal Methods for Industrial Critical Systems: 19th International Conference, FMICS 2014, Florence, Italy, September 11-12, 2014. Proceedings. Lang, F. & Flammini, F. (eds.). Springer, p. 185-199 15 p. (Lecture Notes in Computer Science; vol. 8718).

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

    Open Access
    File
  • 2012

    An Executable Semantics for CompCert C

    Campbell, B., 2012, Certified Programs and Proofs: Second International Conference, CPP 2012, Kyoto, Japan, December 13-15, 2012. Proceedings. Hawblitzel, C. & Miller, D. (eds.). Springer, p. 60-75 16 p. (Lecture Notes in Computer Science; vol. 7679).

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

    Open Access
    File
  • 2009

    Amortised Memory Analysis Using the Depth of Data Structures

    Campbell, B., 2009, Programming Languages and Systems: 18th European Symposium on Programming, ESOP 2009, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2009, York, UK, March 22-29, 2009. Proceedings. Castagna, G. (ed.). Springer, p. 190-204 15 p. (Lecture Notes in Computer Science; vol. 5502).

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

    Open Access
    File
  • 2008

    Prediction of linear memory usage for first-order functional programs

    Campbell, B., 2008, Proceedings of the Nineth Symposium on Trends in Functional Programming, TFP 2008, Nijmegen, The Netherlands, May 26-28, 2008.. p. 1-16 16 p.

    Research output: Chapter in Book/Report/Conference proceedingConference contribution