|
2019 Journal Article Linearizability on hardware weak memory modelsSmith, Graeme, Winter, Kirsten and Colvin, Robert J. (2019). Linearizability on hardware weak memory models. Formal Aspects of Computing, 32 (1), 1-32. doi: 10.1007/s00165-019-00499-8 |
|
2019 Conference Publication Value-dependent information-flow security on weak memory modelsSmith, Graeme, Coughlin, Nicholas and Murray, Toby (2019). Value-dependent information-flow security on weak memory models. Third World Congress, FM 2019, Porto, Portugal, 7-11 October 2019. Cham, Switzerland: Springer. doi: 10.1007/978-3-030-30942-8_32 |
|
2018 Conference Publication A wide-spectrum language for verification of programs on weak memory modelsColvin, Robert J. and Smith, Graeme (2018). A wide-spectrum language for verification of programs on weak memory models. 22nd International Symposium on Formal Methods, FM 2018 Held as Part of the Federated Logic Conference, FloC 2018, Oxford, United Kingdom, 15-17 July 2018. Heidelberg, Germany: Springer. doi: 10.1007/978-3-319-95582-7_14 |
|
2017 Journal Article Relating trace refinement and linearizabilitySmith, Graeme and Winter, Kirsten (2017). Relating trace refinement and linearizability. Formal Aspects of Computing, 29 (6), 1-16. doi: 10.1007/s00165-017-0418-2 |
|
2016 Journal Article Formal development of multi-agent systems using MAZELi, Qin and Smith, Graeme (2016). Formal development of multi-agent systems using MAZE. Science of Computer Programming, 131, 126-150. doi: 10.1016/j.scico.2016.04.008 |
|
2012 Journal Article Emergence and refinementSanders, J. W. and Smith, Graeme (2012). Emergence and refinement. Formal Aspects of Computing, 24 (1), 45-65. doi: 10.1007/s00165-011-0190-7 |
|
1999 Book The Object-Z Specification LanguageSmith, G. P. (1999). The Object-Z Specification Language. Boston: Kluwer Academic Publishers. doi: 10.1007/978-1-4615-5265-9 |
|
2024 Book Chapter Detecting Speculative Execution Vulnerabilities on Weak Memory ModelsCoughlin, Nicholas, Lam, Kait, Smith, Graeme and Winter, Kirsten (2024). Detecting Speculative Execution Vulnerabilities on Weak Memory Models. Lecture Notes in Computer Science. (pp. 482-500) Cham: Springer Nature Switzerland. doi: 10.1007/978-3-031-71162-6_25 |
|
2024 Journal Article On formal methods thinking in computer science educationDongol, Brijesh, Dubois, Catherine, Hallerstede, Stefan, Hehner, Eric, Morgan, Carroll, Müller, Peter, Ribeiro, Leila, Silva, Alexandra, Smith, Graeme and de Vink, Erik (2024). On formal methods thinking in computer science education. Formal Aspects of Computing, 37 (1) 8, 1-23. doi: 10.1145/3670419 |
|
2023 Journal Article Compositional reasoning for non-multicopy atomic architecturesCoughlin, Nicholas, Winter, Kirsten and Smith, Graeme (2023). Compositional reasoning for non-multicopy atomic architectures. Formal Aspects of Computing, 35 (2) 8, 1-30. doi: 10.1145/3574137 |
|
2023 Conference Publication A Dafny-based approach to thread-local information flow analysisSmith, Graeme (2023). A Dafny-based approach to thread-local information flow analysis. IEEE/ACM 11th International Conference on Formal Methods in Software Engineering (FormaliSE), Melbourne, VIC, Australia, 14-15 May 2023. Piscataway, NJ, United States: IEEE. doi: 10.1109/formalise58978.2023.00017 |
|
2022 Journal Article Compositional noninterference on hardware weak memory modelsCoughlin, Nicholas and Smith, Graeme (2022). Compositional noninterference on hardware weak memory models. Science of Computer Programming, 217 102779, 1-23. doi: 10.1016/j.scico.2022.102779 |
|
2022 Conference Publication Declassification predicates for controlled information releaseSmith, Graeme (2022). Declassification predicates for controlled information release. 23rd International Conference on Formal Engineering Methods, ICFEM 2022, Madrid, Spain, 24-27 October 2022. Heidelberg, Germany: Springer. doi: 10.1007/978-3-031-17244-1_18 |
|
2021 Journal Article Information-flow control on ARM and POWER multicore processorsSmith, Graeme, Coughlin, Nicholas and Murray, Toby (2021). Information-flow control on ARM and POWER multicore processors. Formal Methods in System Design, 58 (1-2), 251-293. doi: 10.1007/s10703-021-00376-2 |
|
2021 Conference Publication Backwards-directed information flow analysis for concurrent programsWinter, Kirsten, Coughlin, Nicholas and Smith, Graeme (2021). Backwards-directed information flow analysis for concurrent programs. Computer Security Foundations Symposium, Dubrovnik, Croatia, 21-25 June 2021. Piscataway, NJ, United States: IEEE. doi: 10.1109/csf51468.2021.00017 |
|
2021 Conference Publication Rely/guarantee reasoning for multicopy atomic weak memory modelsCoughlin, Nicholas, Winter, Kirsten and Smith, Graeme (2021). Rely/guarantee reasoning for multicopy atomic weak memory models. 24th International Symposium on Formal Methods (FM), Virtual, 20-26 November 2021. Cham, Switzerland: Springer Science and Business Media Deutschland. doi: 10.1007/978-3-030-90870-6_16 |
|
2020 Conference Publication Rely/guarantee reasoning for noninterference in non-blocking algorithmsCoughlin, Nicholas and Smith, Graeme (2020). Rely/guarantee reasoning for noninterference in non-blocking algorithms. 33rd IEEE Computer Security Foundations Symposium (CSF), Boston, MA, United States, 22-26 June 2020. Piscataway, NJ, United States: IEEE. doi: 10.1109/csf49147.2020.00034 |
|
2020 Conference Publication Specification with class: a brief history of object-ZSmith, Graeme and Duke, David J. (2020). Specification with class: a brief history of object-Z. 23rd Symposium on Formal Methods, FM 2019, Porto, Portugal, 7-11 October 2019. Cham, Switzerland: Springer Cham. doi: 10.1007/978-3-030-54997-8_4 |
|
2020 Conference Publication Weakening correctness and linearizability for concurrent objects on multicore processorsSmith, Graeme and Groves, Lindsay (2020). Weakening correctness and linearizability for concurrent objects on multicore processors. Formal Methods. FM 2019 International Workshops, Porto, Portugal, 7-11 October 2019. Heidelberg, Germany: Springer. doi: 10.1007/978-3-030-54997-8_22 |
|
2019 Journal Article Modelling concurrent objects running on the TSO and ARMv8 memory modelsWinter, Kirsten, Smith, Graeme and Derrick, John (2019). Modelling concurrent objects running on the TSO and ARMv8 memory models. Science of Computer Programming, 184 102308, 102308. doi: 10.1016/j.scico.2019.102308 |
