|
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 |
|
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 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 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 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. |
|
2018 Conference Publication Observational models for linearizability checking on weak memory modelsWinter, Kirsten, Smith, Graeme and Derrick, John (2018). Observational models for linearizability checking on weak memory models. International Symposium on Theoretical Aspects of Software Engineering (TASE), Guangzhou, China, 29-31 August 2018. Piscataway, NJ United States: IEEE. doi: 10.1109/TASE.2018.00021 |
|
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 |
|
2017 Conference Publication An observational approach to defining linearizability on weak memory modelsDerrick, John and Smith, Graeme (2017). An observational approach to defining linearizability on weak memory models. Formal Techniques for Distributed Objects, Components, and Systems, Neuchâtel, Switzerland, 19–22 June 2017. Heidelberg, Germany: Springer . doi: 10.1007/978-3-319-60225-7_8 |
|
2017 Conference Publication Improving the Scalability of Automatic Linearizability Checking in SPINDoolan, Patrick, Smith, Graeme, Zhang, Chenyi and Krishnan, Padmanabhan (2017). Improving the Scalability of Automatic Linearizability Checking in SPIN. 19th International Conference on Formal Engineering Methods, ICFEM 2017, Xi'an,, November 13, 2017-November 17, 2017. Cham, Switzerland: Springer Verlag. doi: 10.1007/978-3-319-68690-5_7 |
|
2016 Conference Publication Model checking simulation rules for linearizabilitySmith, Graeme (2016). Model checking simulation rules for linearizability. 14th International Conference on Software Engineering and Formal Methods, SEFM 2016, Vienna, Austria, 4-8 July 2016. Heidelberg, Germany: Springer. doi: 10.1007/978-3-319-41591-8_13 |
|
2016 Conference Publication Invariant generation for linearizability proofsSmith, Graeme and Derrick, John (2016). Invariant generation for linearizability proofs. 31st Annual ACM Symposium on Applied Computing, SAC 2016, Pisa, Italy, 4 - 8 April 2016. New York, NY, United States: Association for Computing Machinery. doi: 10.1145/2851613.2851837 |
|
2015 Conference Publication A macro-level model for investigating the effect of directional bias on network coverageSmith, Graeme, Sanders, J. W. and Li, Qin (2015). A macro-level model for investigating the effect of directional bias on network coverage. 38th Australasian Computer Science Conference (ACSC 2015), Sydney, Australia, 27-30 January 2015. Sydney, Australia: Australian Computer Society. |
|
2015 Conference Publication Admit your weakness: Verifying correctness on TSO architecturesSmith, Graeme, Derrick, John and Dongol, Brijesh (2015). Admit your weakness: Verifying correctness on TSO architectures. 11th International Symposium on Formal Aspects of Component Software, FACS 2014, Bertinoro, Italy, 10 - 12 September 2014. Heidelberg, Germany: Springer Verlag. doi: 10.1007/978-3-319-15317-9_22 |
|
2015 Conference Publication Defining correctness conditions for concurrent objects in multicore architecturesDongol, Brijesh, Derrick, John, Groves, Lindsay and Smith, Graeme (2015). Defining correctness conditions for concurrent objects in multicore architectures. 29th European Conference on Object-Oriented Programming, ECOOP 2015, Prague, Czech Republic, 5-10 July 2015. Wadern, Germany: Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing. doi: 10.4230/LIPIcs.ECOOP.2015.470 |
|
2015 Conference Publication Using Z in the development and maintenance of computational models of real-world systemsMoeiniyan Bagheri, Shahrzad, Smith, Graeme and Hanan, Jim (2015). Using Z in the development and maintenance of computational models of real-world systems. 12th International Conference on Software Engineering and Formal Methods, Grenoble, France, 1 - 2 September 2014. Heidelberg, Germany: Springer Verlag. doi: 10.1007/978-3-319-15201-1_3 |
