Skip to menu Skip to content Skip to footer

2019

Conference Publication

Preface

Dongol, 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.

Preface

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, Proceedings

Brijesh 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.

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

2018

Conference Publication

Correctness of concurrent objects under weak memory models

Smith, 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

Correctness of concurrent objects under weak memory models

2018

Conference Publication

Observational models for linearizability checking on weak memory models

Winter, 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

Observational models for linearizability checking on weak memory models

2017

Conference Publication

An observational approach to defining linearizability on weak memory models

Derrick, 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

An observational approach to defining linearizability on weak memory models

2017

Conference Publication

Improving the Scalability of Automatic Linearizability Checking in SPIN

Doolan, 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

Improving the Scalability of Automatic Linearizability Checking in SPIN

2017

Book Chapter

A proof method for linearizability on TSO architectures

Derrick, John, Smith, Graeme, Groves, Lindsay and Dongol, Brijesh (2017). A proof method for linearizability on TSO architectures. Provably correct systems. (pp. 61-91) edited by Mike Hinchey, Jonathan P. Bowen and Ernst-Rüdiger Olderog. Cham, Switzerland: Springer International Publishing. doi: 10.1007/978-3-319-48628-4

A proof method for linearizability on TSO architectures

2016

Journal Article

Refining autonomous agents with declarative beliefs and desires

Li, Qin and Smith, Graeme (2016). Refining autonomous agents with declarative beliefs and desires. Formal Aspects of Computing, 29 (2), 1-23. doi: 10.1007/s00165-016-0391-1

Refining autonomous agents with declarative beliefs and desires

2016

Conference Publication

Invariant generation for linearizability proofs

Smith, 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

Invariant generation for linearizability proofs

2016

Conference Publication

Model checking simulation rules for linearizability

Smith, 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

Model checking simulation rules for linearizability

2015

Conference Publication

Using Z in the development and maintenance of computational models of real-world systems

Moeiniyan 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

Using Z in the development and maintenance of computational models of real-world systems

2015

Conference Publication

A framework for correctness criteria on weak memory models

Derrick, John and Smith, Graeme (2015). A framework for correctness criteria on weak memory models. 20th International Symposium on Formal Methods, FM 2015, Oslo, Norway, 25-26 June 2015. Heidelberg, Germany: Springer. doi: 10.1007/978-3-319-19249-9_12

A framework for correctness criteria on weak memory models

2015

Conference Publication

A macro-level model for investigating the effect of directional bias on network coverage

Smith, 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.

A macro-level model for investigating the effect of directional bias on network coverage

2015

Conference Publication

Admit your weakness: Verifying correctness on TSO architectures

Smith, 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

Admit your weakness: Verifying correctness on TSO architectures

2015

Conference Publication

Defining correctness conditions for concurrent objects in multicore architectures

Dongol, 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

Defining correctness conditions for concurrent objects in multicore architectures

2014

Conference Publication

Reasoning algebraically about refinement on TSO architectures

Dongol, Brijesh, Derrick, John and Smith, Graeme (2014). Reasoning algebraically about refinement on TSO architectures. International Colloquium on Theoretical Aspects of Computing, Bucharest, Romania, 17-19 September 2014. Cham, Switzerland: Springer. doi: 10.1007/978-3-319-10882-7_10

Reasoning algebraically about refinement on TSO architectures

2014

Book Chapter

Designing adaptive systems using teleo-reactive agents

Smith, Graeme, Sanders, J. W. and Winter, Kirsten (2014). Designing adaptive systems using teleo-reactive agents. Transactions on Computational Collective Intelligence XVI. (pp. 34-61) edited by Ryszard Kowalczyk and Ngoc Thanh Nguyen. Heidelberg, Germany: Springer. doi: 10.1007/978-3-662-44871-7_2

Designing adaptive systems using teleo-reactive agents

2014

Conference Publication

A formal development approach for self-organising systems

Li, Q. and Smith, G. (2014). A formal development approach for self-organising systems. 8th International Symposium on Theoretical Aspects of Software Engineering, TASE 2014, Changsha, Hunan, China, 1-3 September 2014. Los Alamitos, CA United States: IEEE Computer Society. doi: 10.1109/TASE.2014.11

A formal development approach for self-organising systems

2014

Conference Publication

MAZE: An extension of object-Z for multi-agent systems

Smith, Graeme and Li, Qin (2014). MAZE: An extension of object-Z for multi-agent systems. 4th International Conference on Abstract State Machines, Alloy, B, TLA, VDM, and Z, ABZ 2014, Toulouse, France, June 2, 2014-June 6, 2014. Heidelberg, Germany: Springer. doi: 10.1007/978-3-662-43652-3_6

MAZE: An extension of object-Z for multi-agent systems

2014

Conference Publication

Verifying linearizability on TSO architectures

Derrick, John, Smith, Graeme and Dongol, Brijesh (2014). Verifying linearizability on TSO architectures. 11th International Conference on Integrated Formal Methods, IFM 2014, Bertinoro, Italy, 9 - 11 September 2014. Heidelberg, Germany: Springer. doi: 10.1007/978-3-319-10181-1_21

Verifying linearizability on TSO architectures