default search action
Graeme Smith 0001
Person information
- affiliation: University of Queensland, School of Information Technology and Electrical Engineering, Brisbane, Australia
- affiliation: Defence Science and Technology Group, Brisbane, Australia
Other persons with the same name
- Graeme Smith — disambiguation page
- Graeme Smith 0002 — University of Waterloo, ON, Canada (and 1 more)
Refine list
refinements active!
zoomed in on ?? of ?? records
view refined list in
export refined list as
showing all ?? records
2020 – today
- 2024
- [c72]Nicholas Coughlin
, Kait Lam
Detecting Speculative Execution Vulnerabilities on Weak Memory Models. FM (1) 2024: 482-500 - 2023
- [j23]Nicholas Coughlin
Compositional Reasoning for Non-multicopy Atomic Architectures. Formal Aspects Comput. 35(2): 8:1-8:30 (2023) - [c71]Graeme Smith
A Dafny-based approach to thread-local information flow analysis. FormaliSE 2023: 86-96 - 2022
- [j22]Nicholas Coughlin
Compositional noninterference on hardware weak memory models. Sci. Comput. Program. 217: 102779 (2022) - [c70]Graeme Smith
Declassification Predicates for Controlled Information Release. ICFEM 2022: 298-315 - 2021
- [j21]Graeme Smith
Information-flow control on ARM and POWER multicore processors. Formal Methods Syst. Des. 58(1-2): 251-293 (2021) - [c69]Kirsten Winter, Nicholas Coughlin
Backwards-directed information flow analysis for concurrent programs. CSF 2021: 1-16 - [c68]Nicholas Coughlin, Kirsten Winter, Graeme Smith
Rely/Guarantee Reasoning for Multicopy Atomic Weak Memory Models. FM 2021: 292-310 - 2020
- [j20]Graeme Smith
Linearizability on hardware weak memory models. Formal Aspects Comput. 32(1): 1-32 (2020) - [c67]Nicholas Coughlin
Rely/Guarantee Reasoning for Noninterference in Non-Blocking Algorithms. CSF 2020: 380-394
2010 – 2019
- 2019
- [j19]Kirsten Winter
Modelling concurrent objects running on the TSO and ARMv8 memory models. Sci. Comput. Program. 184 (2019) - [c66]Graeme Smith
Specification with Class: A Brief History of Object-Z. FM Workshops (2) 2019: 73-86 - [c65]Graeme Smith
Weakening Correctness and Linearizability for Concurrent Objects on Multicore Processors. FM Workshops (2) 2019: 342-357 - [c64]Graeme Smith
Value-Dependent Information-Flow Security on Weak Memory Models. FM 2019: 539-555 - [e5]Brijesh Dongol, Luigia Petre, Graeme Smith:
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. Lecture Notes in Computer Science 11758, Springer 2019, ISBN 978-3-030-32440-7 [contents] - 2018
- [c63]Robert J. Colvin, Graeme Smith
A Wide-Spectrum Language for Verification of Programs on Weak Memory Models. FM 2018: 240-257 - [c62]Kirsten Winter, Graeme Smith
Observational Models for Linearizability Checking on Weak Memory Models. TASE 2018: 100-107 - [c61]Graeme Smith
Correctness of Concurrent Objects under Weak Memory Models. Refine@FM 2018: 53-67 - [i4]Robert J. Colvin, Graeme Smith:
A wide-spectrum language for verification of programs on weak memory models. CoRR abs/1802.04406 (2018) - [i3]Graeme Smith, Kirsten Winter, Robert J. Colvin:
A sound and complete definition of linearizability on weak memory models. CoRR abs/1802.04954 (2018) - [i2]Robert J. Colvin, Graeme Smith:
A high-level operational semantics for hardware weak memory models. CoRR abs/1812.00996 (2018) - 2017
- [j18]Qin Li, Graeme Smith
Refining autonomous agents with declarative beliefs and desires. Formal Aspects Comput. 29(2): 227-249 (2017) - [j17]Graeme Smith
Relating trace refinement and linearizability. Formal Aspects Comput. 29(6): 935-950 (2017) - [c60]John Derrick
An Observational Approach to Defining Linearizability on Weak Memory Models. FORTE 2017: 108-123 - [c59]Patrick Doolan, Graeme Smith
Improving the Scalability of Automatic Linearizability Checking in SPIN. ICFEM 2017: 105-121 - [p2]John Derrick, Graeme Smith, Lindsay Groves, Brijesh Dongol:
A Proof Method for Linearizability on TSO Architectures. Provably Correct Systems 2017: 61-91 - 2016
- [j16]Qin Li
Formal development of multi-agent systems using MAZE. Sci. Comput. Program. 131: 126-150 (2016) - [c58]Graeme Smith
Invariant generation for linearizability proofs. SAC 2016: 1694-1699 - [c57]Graeme Smith
Model Checking Simulation Rules for Linearizability. SEFM 2016: 188-203 - 2015
- [c56]Graeme Smith, Jeff W. Sanders, Qin Li:
A Macro-Level Model for Investigating the E ect of Directional Bias on Network Coverage. ACSC 2015: 73-81 - [c55]Brijesh Dongol
Defining Correctness Conditions for Concurrent Objects in Multicore Architectures. ECOOP 2015: 470-494 - [c54]John Derrick
A Framework for Correctness Criteria on Weak Memory Models. FM 2015: 178-194 - 2014
- [j15]Graeme Smith
Designing Adaptive Systems Using Teleo-Reactive Agents. Trans. Comput. Collect. Intell. 16: 34-61 (2014) - [c53]Graeme Smith
MAZE: An Extension of Object-Z for Multi-Agent Systems. ABZ 2014: 72-85 - [c52]Graeme Smith
On Directional Bias for Network Coverage. BIC-TA 2014: 384-388 - [c51]Graeme Smith
Admit Your Weakness: Verifying Correctness on TSO Architectures. FACS 2014: 364-383 - [c50]John Derrick, Graeme Smith
Using Coarse-Grained Abstractions to Verify Linearizability on TSO Architectures. Haifa Verification Conference 2014: 1-16 - [c49]Brijesh Dongol
Reasoning Algebraically About Refinement on TSO Architectures. ICTAC 2014: 151-168 - [c48]John Derrick
Verifying Linearizability on TSO Architectures. IFM 2014: 341-356 - [c47]Shahrzad Moeiniyan Bagheri, Graeme Smith
Using Z in the Development and Maintenance of Computational Models of Real-World Systems. SEFM Workshops 2014: 36-53 - [c46]Qin Li, Graeme Smith
A Formal Development Approach for Self-Organising Systems. TASE 2014: 209-212 - [i1]Graeme Smith, Jeff W. Sanders, Qin Li:
A macro-level model for investigating the effect of directional bias on network coverage. CoRR abs/1407.5762 (2014) - 2013
- [c45]Qin Li, Graeme Smith
Using Bounded Fairness to Specify and Verify Ordered Asynchronous Multi-agent Systems. ICECCS 2013: 111-120 - [c44]Qin Li, Graeme Smith
A Refinement Framework for Autonomous Agents. SBMF 2013: 163-178 - 2012
- [j14]Jeff W. Sanders, Graeme Smith
Emergence and refinement. Formal Aspects Comput. 24(1): 45-65 (2012) - [j13]John Derrick
Temporal-logic property preservation under Z refinement. Formal Aspects Comput. 24(3): 393-416 (2012) - [c43]Graeme Smith
Reasoning About Adaptivity of Agents and Multi-agent Systems. ICECCS 2012: 341-350 - [c42]Graeme Smith
Using conventional reasoning techniques for self-organising systems. PST 2012: 238-243 - [c41]Graeme Smith
Incremental Development of Multi-agent Systems in Object-Z. SEW 2012: 120-129 - 2011
- [j12]Zheng Fu, Graeme Smith
Property transformation under specification change. Frontiers Comput. Sci. China 5(1): 1-13 (2011) - [c40]Graeme Smith
Refactoring Object-Oriented Specifications with Inheritance-Based Polymorphism. TASE 2011: 35-41 - 2010
- [j11]Eerke A. Boiten
Editorial. Formal Aspects Comput. 22(1): 1 (2010) - [c39]Aaron Sampson, Graeme Smith
Gravity Points in Potential-Field Approaches to Self Organisation. SASO Workshops 2010: 110-115 - [c38]Sebastian Eder, Graeme Smith
An Approach to Formal Verification of Free-Flight Separation. SASO Workshops 2010: 166-171 - [c37]Jeff W. Sanders, Graeme Smith
Assuring Adaptive Behaviour in Self-Organising Systems. SASO Workshops 2010: 172-177
2000 – 2009
- 2009
- [j10]Graeme Smith
Model checking action system refinements. Formal Aspects Comput. 21(1-2): 155-186 (2009) - [c36]Graeme Smith
Formal Development of Self-organising Systems. ATC 2009: 90-104 - [c35]Jeff W. Sanders, Graeme Smith
Refining Emergent Properties. REFINE@FMWeek 2009: 207-223 - 2008
- [c34]Tim McComb, Graeme Smith
Introducing Objects through Refinement. FM 2008: 358-373 - [c33]Tim McComb, Graeme Smith
A Minimal Set of Refactoring Rules for Object-Z. FMOODS 2008: 170-184 - [c32]Zheng Fu, Graeme Smith
Towards More Flexible Development of Z Specifications. TASE 2008: 281-288 - [c31]Graeme Smith
Refactoring Real-time Specifications. Refine@FM 2008: 359-380 - [p1]Jeffrey W. Sanders, Graeme Smith:
Formal Ensemble Engineering. Software-Intensive Systems and New Computing Paradigms 2008: 132-138 - [e4]Eerke A. Boiten, John Derrick, Graeme Smith:
Proceedings of the BCS-FACS Refinement Workshop, REFINE@IFM 2007, Oxford, UK, July 2007. Electronic Notes in Theoretical Computer Science 201, Elsevier 2008 [contents] - 2007
- [c30]Larissa Meinicke
A Stepwise Development Process for Reasoning About the Reliability of Real-Time Systems. IFM 2007: 439-458 - [c29]Eerke A. Boiten
Preface. REFINE@IFM 2007: 1 - [c28]John Derrick
Using Model Checking to Automatically Find Retrieve Relations. REFINE@IFM 2007: 155-175 - [e3]Judi Romijn, Graeme Smith, Jaco van de Pol:
Proceedings of the Doctoral Symposium affiliated with the Fifth Integrated Formal Methods Conference, IFM Doctoral Symposium 2005, Eindhoven, The Netherlands, November 29, 2005. Electronic Notes in Theoretical Computer Science 191, Elsevier 2007 [contents] - 2006
- [j9]Graeme Smith
Verifying data refinements using a model checker. Formal Aspects Comput. 18(3): 264-287 (2006) - [c27]Tim McComb, Graeme Smith:
Compositional Class Refinement in Object-Z. FM 2006: 205-220 - [c26]Graeme Smith
Simulation Machines for Checking Action System Refinements. Refine@ICFEM 2006: 75-90 - 2005
- [j8]Eerke A. Boiten
Guest Editorial Integrated Formal Methods. Formal Aspects Comput. 17(4): 389-389 (2005) - [c25]Graeme Smith
Model Checking Z Specifications Using SAL. ZB 2005: 85-103 - [c24]Judi Romijn, Graeme Smith
Preface. IFM Doctoral Symposium 2005: 1-2 - [c23]Graeme Smith
Model Checking Downward Simulations. REFINE 2005: 205-224 - [e2]Judi Romijn, Graeme Smith, Jaco van de Pol:
Integrated Formal Methods, 5th International Conference, IFM 2005, Eindhoven, The Netherlands, November 29 - December 2, 2005, Proceedings. Lecture Notes in Computer Science 3771, Springer 2005, ISBN 3-540-30492-4 [contents] - 2004
- [c22]John Derrick, Graeme Smith
Linear Temporal Logic and Z Refinement. AMAST 2004: 117-131 - [c21]Tim McComb, Graeme Smith
Architectural Design in Object-Z. Australian Software Engineering Conference 2004: 77-86 - [e1]Eerke A. Boiten
Integrated Formal Methods, 4th International Conference, IFM 2004, Canterbury, UK, April 4-7, 2004, Proceedings. Lecture Notes in Computer Science 2999, Springer 2004, ISBN 3-540-21377-5 [contents] - 2003
- [j7]John Derrick
Structural Refinement of Systems Specified in Object-Z and CSP. Formal Aspects Comput. 15(1): 1-27 (2003) - [c20]Tim McComb, Graeme Smith
Animation of Object-Z Specifications Using a Z Animator. SEFM 2003: 191- - [c19]Graeme Smith, Kirsten Winter:
Proving Temporal Properties of Z Specifications Using Abstraction. ZB 2003: 260-279 - [c18]Kirsten Winter, Graeme Smith
Compositional Verification for Object-Z. ZB 2003: 280-299 - 2002
- [j6]Graeme Smith
An Introduction to Real-Time Object-Z. Formal Aspects Comput. 13(2): 128-141 (2002) - [c17]Graeme Smith
Abstract Specification in Object-Z and CSP. ICFEM 2002: 108-119 - [c16]Graeme Smith
Introducing Reference Semantics via Refinement. ICFEM 2002: 588-599 - [c15]Graeme Smith
An Integration of Real-Time Object-Z and CSP for Specifying Concurrent Real-Time Systems. IFM 2002: 267-285 - [c14]Graeme Smith
Encoding Object-Z in Isabelle/HOL. ZB 2002: 82-99 - 2001
- [j5]Graeme Smith
Specification, Refinement and Verification of Concurrent Systems-An Integration of Object-Z and CSP. Formal Methods Syst. Des. 18(3): 249-284 (2001) - [c13]Geoff Kassel, Graeme Smith
Model Checking Object-Z Classes: Some Experiments with FDR. APSEC 2001: 445-452 - 2000
- [j4]Graeme Smith, Colin J. Fidge:
Incremental Development of Real-Time Requirements: The Light Control Case Study. J. Univers. Comput. Sci. 6(7): 704-730 (2000) - [c12]Graeme Smith
Stepwise Development from Ideal Specifications. ACSC 2000: 227-233 - [c11]Graeme Smith
Structuring Real-Time Object-Z Specifications. IFM 2000: 97-115 - [c10]John Derrick, Graeme Smith
Structural Refinement in Object-Z/CSP. IFM 2000: 194-213
1990 – 1999
- 1999
- [c9]Graeme Smith
Towards Real-Time Object-Z. IFM 1999: 49-65 - 1997
- [c8]Graeme Smith
A Semantic Integration of Object-Z and CSP for the Specification of Concurrent Systems. FME 1997: 62-81 - [c7]Clemens Fischer, Graeme Smith:
Combining CSP and Object-Z: Finite or Infinite Trace Semantics? FORTE 1997: 503-518 - [c6]Graeme Smith, John Derrick:
Refinement and Verification of Concurrent Systems Specified in Object-Z and CSP. ICFEM 1997: 293-303 - 1996
- [j3]Roger Duke, Cecily Bailes, Graeme Smith
A Blocking Model for Reactive Objects. Formal Aspects Comput. 8(3): 347-368 (1996) - 1995
- [j2]Graeme Smith
A Fully Abstract Semantics of Classes for Object-Z. Formal Aspects Comput. 7(3): 289-313 (1995) - 1994
- [c5]Graeme Smith
Formal definitions of behavioural compatibility for active and passive objects. APSEC 1994: 336-344 - 1992
- [b1]Graeme Smith:
An object-oriented approach to formal specification. University of Queensland, Australia, 1992 - 1991
- [c4]Roger Duke, Paul King, Gordon A. Rose, Graeme Smith:
Associated Paper: The Object-Z Specification Language. TOOLS (5) 1991: 465-484 - 1990
- [c3]Roger Duke, Gordon A. Rose, Graeme Smith:
Transferring Formal Techniques to Industry. FORTE 1990: 279-286 - [c2]Paul King, Graeme Smith:
Formalisation of behavioural and structural concepts for communication systems. PSTV 1990: 3-18
1980 – 1989
- 1989
- [j1]Roger Duke, Graeme Smith:
Temporal Logic and Z Specifications. Aust. Comput. J. 21(2): 62-66 (1989) - [c1]David A. Carrington, David J. Duke, Roger Duke, Paul King, Gordon A. Rose, Graeme Smith:
Object-Z: An Object-Oriented Extension to Z. FORTE 1989: 281-296
Coauthor Index
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
Unpaywalled article links
Add open access links from to the list of external document links (if available).
Privacy notice: By enabling the option above, your browser will contact the API of unpaywall.org to load hyperlinks to open access articles. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Unpaywall privacy policy.
Archived links via Wayback Machine
For web page which are no longer available, try to retrieve content from the of the Internet Archive (if available).
Privacy notice: By enabling the option above, your browser will contact the API of archive.org to check for archived content of web pages that are no longer available. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Internet Archive privacy policy.
Reference lists
Add a list of references from ,
, and
to record detail pages.
load references from crossref.org and opencitations.net
Privacy notice: By enabling the option above, your browser will contact the APIs of crossref.org, opencitations.net, and semanticscholar.org to load article reference information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Crossref privacy policy and the OpenCitations privacy policy, as well as the AI2 Privacy Policy covering Semantic Scholar.
Citation data
Add a list of citing articles from and
to record detail pages.
load citations from opencitations.net
Privacy notice: By enabling the option above, your browser will contact the API of opencitations.net and semanticscholar.org to load citation information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the OpenCitations privacy policy as well as the AI2 Privacy Policy covering Semantic Scholar.
OpenAlex data
Load additional information about publications from .
Privacy notice: By enabling the option above, your browser will contact the API of openalex.org to load additional information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the information given by OpenAlex.
last updated on 2024-10-07 21:17 CEST by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by: