|
2025 Conference Publication Detecting speculative data flow vulnerabilities using weakest precondition reasoningSmith, Graeme (2025). Detecting speculative data flow vulnerabilities using weakest precondition reasoning. 19th International Symposium, Limassol, Cyprus, 14-16 July 2025. Cham, Switzerland: Springer Cham. doi: 10.1007/978-3-031-98208-8_19 |
|
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 Other Outputs Automatic linearizability checking of operations on concurrent data structuresDoolan, Patrick James, Zhang, Chenyi, Smith, Graeme Paul and Krishnan, Padmanabhan (2020). Automatic linearizability checking of operations on concurrent data structures. 10552408. |
|
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 |
|
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 |
|
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 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 |
|
2019 Edited Outputs Formal methods teaching: Third International Workshop and Tutorial, FMTea 2019, Held as Part of the Third World Congress on Formal Methods, FM 2019, Porto, Portugal, October 7, 2019, ProceedingsBrijesh Dongol, Luigia Petre and Graeme Smith eds. (2019). Formal methods teaching: Third International Workshop and Tutorial, FMTea 2019, Held as Part of the Third World Congress on Formal Methods, FM 2019, Porto, Portugal, October 7, 2019, Proceedings. Formal Methods Teaching: Third International Workshop and Tutorial, FMTea 2019, Held as Part of the Third World Congress on Formal Methods, FM 2019, Porto, Portugal, 7 October 2019. Cham, Switzerland: Springer International Publishing. |
|
2019 Conference Publication PrefaceDongol, Brijesh, Petre, Luigia and Smith, Graeme (2019). Preface. Third International Workshop and Tutorial, FMTea 2019, Held as Part of the Third World Congress on Formal Methods, Porto, Portugal, 7 October 2019. Cham, Switzerland: Springer. |
|
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 Correctness of concurrent objects under weak memory modelsSmith, Graeme, Winter, Kirsten and Colvin, Robert J. (2018). Correctness of concurrent objects under weak memory models. 18th Refinement Workshop, Refine 2018, Oxford, United Kingdom, 18 July 2018. SYDNEY: Open Publishing Association. doi: 10.4204/EPTCS.282.5 |
