| Modelling the ARMv8 architecture, operationally: Concurrency and ISA S Flur, KE Gray, C Pulte, S Sarkar, A Sezgin, L Maranget, W Deacon, ... Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of …, 2016 | 175 | 2016 |
| Simplifying ARM concurrency: multicopy-atomic axiomatic and operational models for ARMv8 C Pulte, S Flur, W Deacon, J French, S Sarkar, P Sewell Proceedings of the ACM on Programming Languages 2 (POPL), 1-29, 2017 | 154 | 2017 |
| 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), 1-31, 2019 | 109 | 2019 |
| An integrated concurrency and core-ISA architectural envelope definition, and test oracle, for IBM POWER multiprocessors KE Gray, G Kerneis, D Mulligan, C Pulte, S Sarkar, P Sewell Proceedings of the 48th International Symposium on Microarchitecture, 635-646, 2015 | 47 | 2015 |
| Mixed-size concurrency: ARM, Power, C/C++ 11, and SC S Flur, S Sarkar, C Pulte, K Nienhuis, L Maranget, KE Gray, A Sezgin, ... ACM SIGPLAN Notices 52 (1), 429-442, 2017 | 44 | 2017 |
| Promising-ARM/RISC-V: a simpler and faster operational concurrency model C Pulte, J Pichon-Pharabod, J Kang, SH Lee, CK Hur Proceedings of the 40th ACM SIGPLAN Conference on Programming Language …, 2019 | 42 | 2019 |
| Repairing and mechanising the JavaScript relaxed memory model C Watt, C Pulte, A Podkopaev, G Barbier, S Dolan, S Flur, ... Proceedings of the 41st ACM SIGPLAN Conference on Programming Language …, 2020 | 20 | 2020 |
| ARMv8-A system semantics: instruction fetch in relaxed architectures B Simner, S Flur, C Pulte, A Armstrong, J Pichon-Pharabod, L Maranget, ... Programming Languages and Systems: 29th European Symposium on Programming …, 2020 | 14 | 2020 |
| 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 |
| 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 | 10 | 2021 |
| Relaxed virtual memory in Armv8-A B Simner, A Armstrong, J Pichon-Pharabod, C Pulte, R Grisenthwaite, ... Programming Languages and Systems: 31st European Symposium on Programming …, 2022 | 9 | 2022 |
| The semantics of multicopy atomic ARMv8 and RISC-V C Pulte University of Cambridge, 2019 | 8 | 2019 |
| The sail instruction-set semantics specification language KE Gray, P Sewell, C Pulte, S Flur, R Norton-Wright Technical report published by Cambridge University, 2017 | 6 | 2017 |
| Sail A Armstrong, T Bauereiss, B Campbell, S Gray, G Kerneis, ... | 3 | 2019 |
| The Sail instruction-set semantics specification language A Armstrong, T Bauereiss, B Campbell, KE Gray, R Norton-Wright, C Pulte, ... | 2 | 2021 |
| Isla: integrating full-scale ISA semantics and axiomatic concurrency models (extended version) A Armstrong, B Campbell, B Simner, C Pulte, P Sewell Formal Methods in System Design, 1-24, 2023 | 1 | 2023 |
| CN: Verifying Systems C Code with Separation-Logic Refinement Types C Pulte, DC Makwana, T Sewell, K Memarian, P Sewell, N Krishnaswami Proceedings of the ACM on Programming Languages 7 (POPL), 1-32, 2023 | 1 | 2023 |
| Relaxed virtual memory in Armv8-A (extended version) B Simner, A Armstrong, J Pichon-Pharabod, C Pulte, R Grisenthwaite, ... arXiv preprint arXiv:2203.00642, 2022 | | 2022 |
| Research data supporting “Mixed-size Concurrency: ARM, POWER, C/C++ 11, and SC” S Flur, S Sarkar, C Pulte, K Nienhuis, L Maranget, KE Gray, A Sezgin, ... University of Cambridge, 2016 | | 2016 |
| An Axiomatic Semantics for Instruction Fetching B Simner, S Flur, C Pulte, A Armstrong, J Pichon-Pharabod, L Maranget, ... | | |
