Graeme Smith - RankMe

109 papers A 3B 18C 16Misc 6Journal 28Unranked 32

Year	Rank	Type	Title / Venue / Authors
2025	Misc	`conf`	Detecting Speculative Data Flow Vulnerabilities Using Weakest Precondition Reasoning. TASE Graeme Smith
2025	J	`jnl`	On Formal Methods Thinking in Computer Science Education. Formal Aspects Comput. Brijesh Dongol, Catherine Dubois, Stefan Hallerstede, Eric C. R. Hehner, Carroll Morgan, Peter Müller, Leila Ribeiro, Alexandra Silva, Graeme Smith, Erik P. de Vink
2024	—	`conf`	Detecting Speculative Execution Vulnerabilities on Weak Memory Models. FM (1) Nicholas Coughlin, Kait Lam, Graeme Smith, Kirsten Winter
2023	—	`conf`	A Dafny-based approach to thread-local information flow analysis. FormaliSE Graeme Smith
2023	J	`jnl`	Compositional Reasoning for Non-multicopy Atomic Architectures. Formal Aspects Comput. Nicholas Coughlin, Kirsten Winter, Graeme Smith
2022	J	`jnl`	Compositional noninterference on hardware weak memory models. Sci. Comput. Program. Nicholas Coughlin, Graeme Smith
2022	C	`conf`	Declassification Predicates for Controlled Information Release. ICFEM Graeme Smith
2021	A	`conf`	Backwards-directed information flow analysis for concurrent programs. CSF Kirsten Winter, Nicholas Coughlin, Graeme Smith
2021	J	`jnl`	Information-flow control on ARM and POWER multicore processors. Formal Methods Syst. Des. Graeme Smith, Nicholas Coughlin, Toby Murray
2021	B	`conf`	Rely/Guarantee Reasoning for Multicopy Atomic Weak Memory Models. FM Nicholas Coughlin, Kirsten Winter, Graeme Smith
2020	J	`jnl`	Linearizability on hardware weak memory models. Formal Aspects Comput. Graeme Smith, Kirsten Winter, Robert J. Colvin
2020	A	`conf`	Rely/Guarantee Reasoning for Noninterference in Non-Blocking Algorithms. CSF Nicholas Coughlin, Graeme Smith
2019	—	`ed.`	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 FMTea Brijesh Dongol, Luigia Petre, Graeme Smith
2019	J	`jnl`	Modelling concurrent objects running on the TSO and ARMv8 memory models. Sci. Comput. Program. Kirsten Winter, Graeme Smith, John Derrick
2019	—	`conf`	Specification with Class: A Brief History of Object-Z. FM Workshops (2) Graeme Smith, David J. Duke
2019	B	`conf`	Value-Dependent Information-Flow Security on Weak Memory Models. FM Graeme Smith, Nicholas Coughlin, Toby Murray
2019	—	`conf`	Weakening Correctness and Linearizability for Concurrent Objects on Multicore Processors. FM Workshops (2) Graeme Smith, Lindsay Groves
2018	B	`conf`	A Wide-Spectrum Language for Verification of Programs on Weak Memory Models. FM Robert J. Colvin, Graeme Smith
2018	J	`jnl`	A high-level operational semantics for hardware weak memory models. CoRR Robert J. Colvin, Graeme Smith
2018	J	`jnl`	A sound and complete definition of linearizability on weak memory models. CoRR Graeme Smith, Kirsten Winter, Robert J. Colvin
2018	J	`jnl`	A wide-spectrum language for verification of programs on weak memory models. CoRR Robert J. Colvin, Graeme Smith
2018	—	`conf`	Correctness of Concurrent Objects under Weak Memory Models. Refine@FM Graeme Smith, Kirsten Winter, Robert J. Colvin
2018	Misc	`conf`	Observational Models for Linearizability Checking on Weak Memory Models. TASE Kirsten Winter, Graeme Smith, John Derrick
2017	—	`ch.`	A Proof Method for Linearizability on TSO Architectures. Provably Correct Systems John Derrick, Graeme Smith, Lindsay Groves, Brijesh Dongol
2017	C	`conf`	An Observational Approach to Defining Linearizability on Weak Memory Models. FORTE John Derrick, Graeme Smith
2017	C	`conf`	Improving the Scalability of Automatic Linearizability Checking in SPIN. ICFEM Patrick Doolan, Graeme Smith, Chenyi Zhang, Padmanabhan Krishnan
2017	J	`jnl`	Refining autonomous agents with declarative beliefs and desires. Formal Aspects Comput. Qin Li, Graeme Smith
2017	J	`jnl`	Relating trace refinement and linearizability. Formal Aspects Comput. Graeme Smith, Kirsten Winter
2016	J	`jnl`	Formal development of multi-agent systems using MAZE. Sci. Comput. Program. Qin Li, Graeme Smith
2016	Misc	`conf`	Invariant generation for linearizability proofs. SAC Graeme Smith, John Derrick
2016	B	`conf`	Model Checking Simulation Rules for Linearizability. SEFM Graeme Smith
2015	B	`conf`	A Framework for Correctness Criteria on Weak Memory Models. FM John Derrick, Graeme Smith
2015	—	`conf`	A Macro-Level Model for Investigating the E ect of Directional Bias on Network Coverage. ACSC Graeme Smith, Jeff W. Sanders, Qin Li
2015	A	`conf`	Defining Correctness Conditions for Concurrent Objects in Multicore Architectures. ECOOP Brijesh Dongol, John Derrick, Lindsay Groves, Graeme Smith
2014	Misc	`conf`	A Formal Development Approach for Self-Organising Systems. TASE Qin Li, Graeme Smith
2014	J	`jnl`	A macro-level model for investigating the effect of directional bias on network coverage. CoRR Graeme Smith, Jeff W. Sanders, Qin Li
2014	—	`conf`	Admit Your Weakness: Verifying Correctness on TSO Architectures. FACS Graeme Smith, John Derrick, Brijesh Dongol
2014	J	`jnl`	Designing Adaptive Systems Using Teleo-Reactive Agents. Trans. Comput. Collect. Intell. Graeme Smith, Jeff W. Sanders, Kirsten Winter
2014	C	`conf`	MAZE: An Extension of Object-Z for Multi-Agent Systems. ABZ Graeme Smith, Qin Li
2014	—	`conf`	On Directional Bias for Network Coverage. BIC-TA Graeme Smith, Jeff W. Sanders, Qin Li
2014	C	`conf`	Reasoning Algebraically About Refinement on TSO Architectures. ICTAC Brijesh Dongol, John Derrick, Graeme Smith
2014	—	`conf`	Using Coarse-Grained Abstractions to Verify Linearizability on TSO Architectures. Haifa Verification Conference John Derrick, Graeme Smith, Lindsay Groves, Brijesh Dongol
2014	—	`conf`	Using Z in the Development and Maintenance of Computational Models of Real-World Systems. SEFM Workshops Shahrzad Moeiniyan Bagheri, Graeme Smith, Jim Hanan
2014	B	`conf`	Verifying Linearizability on TSO Architectures. IFM John Derrick, Graeme Smith, Brijesh Dongol
2013	—	`conf`	A Refinement Framework for Autonomous Agents. SBMF Qin Li, Graeme Smith
2013	B	`conf`	Using Bounded Fairness to Specify and Verify Ordered Asynchronous Multi-agent Systems. ICECCS Qin Li, Graeme Smith
2012	J	`jnl`	Emergence and refinement. Formal Aspects Comput. Jeff W. Sanders, Graeme Smith
2012	C	`conf`	Incremental Development of Multi-agent Systems in Object-Z. SEW Graeme Smith, Kirsten Winter
2012	B	`conf`	Reasoning About Adaptivity of Agents and Multi-agent Systems. ICECCS Graeme Smith, Jeffrey W. Sanders, Kirsten Winter
2012	J	`jnl`	Temporal-logic property preservation under Z refinement. Formal Aspects Comput. John Derrick, Graeme Smith
2012	C	`conf`	Using conventional reasoning techniques for self-organising systems. PST Graeme Smith, Jeff W. Sanders
2011	J	`jnl`	Property transformation under specification change. Frontiers Comput. Sci. China Zheng Fu, Graeme Smith
2011	Misc	`conf`	Refactoring Object-Oriented Specifications with Inheritance-Based Polymorphism. TASE Graeme Smith, Steffen Helke
2010	—	`conf`	An Approach to Formal Verification of Free-Flight Separation. SASO Workshops Sebastian Eder, Graeme Smith
2010	—	`conf`	Assuring Adaptive Behaviour in Self-Organising Systems. SASO Workshops Jeff W. Sanders, Graeme Smith
2010	J	`jnl`	Editorial. Formal Aspects Comput. Eerke A. Boiten, Michael J. Butler, John Derrick, Graeme Smith
2010	—	`conf`	Gravity Points in Potential-Field Approaches to Self Organisation. SASO Workshops Aaron Sampson, Graeme Smith
2009	C	`conf`	Formal Development of Self-organising Systems. ATC Graeme Smith, Jeffrey W. Sanders
2009	J	`jnl`	Model checking action system refinements. Formal Aspects Comput. Graeme Smith, Kirsten Winter
2009	—	`conf`	Refining Emergent Properties. REFINE@FMWeek Jeff W. Sanders, Graeme Smith
2008	—	`conf`	A Minimal Set of Refactoring Rules for Object-Z. FMOODS Tim McComb, Graeme Smith
2008	—	`ch.`	Formal Ensemble Engineering. Software-Intensive Systems and New Computing Paradigms Jeffrey W. Sanders, Graeme Smith
2008	B	`conf`	Introducing Objects through Refinement. FM Tim McComb, Graeme Smith
2008	—	`ed.`	Proceedings of the BCS-FACS Refinement Workshop, REFINE@IFM 2007, Oxford, UK, July 2007 REFINE@IFM Eerke A. Boiten, John Derrick, Graeme Smith
2008	—	`conf`	Refactoring Real-time Specifications. Refine@FM Graeme Smith, Tim McComb
2008	Misc	`conf`	Towards More Flexible Development of Z Specifications. TASE Zheng Fu, Graeme Smith
2007	B	`conf`	A Stepwise Development Process for Reasoning About the Reliability of Real-Time Systems. IFM Larissa Meinicke, Graeme Smith
2007	—	`conf`	Preface. REFINE@IFM Eerke A. Boiten, John Derrick, Graeme Smith
2007	—	`ed.`	Proceedings of the Doctoral Symposium affiliated with the Fifth Integrated Formal Methods Conference, IFM Doctoral Symposium 2005, Eindhoven, The Netherlands, November 29, 2005 IFM Doctoral Symposium Judi Romijn, Graeme Smith, Jaco van de Pol
2007	—	`conf`	Using Model Checking to Automatically Find Retrieve Relations. REFINE@IFM John Derrick, Graeme Smith
2006	B	`conf`	Compositional Class Refinement in Object-Z. FM Tim McComb, Graeme Smith
2006	—	`conf`	Simulation Machines for Checking Action System Refinements. Refine@ICFEM Graeme Smith, Kirsten Winter
2006	J	`jnl`	Verifying data refinements using a model checker. Formal Aspects Comput. Graeme Smith, John Derrick
2005	J	`jnl`	Guest Editorial Integrated Formal Methods. Formal Aspects Comput. Eerke A. Boiten, John Derrick, Graeme Smith
2005	B	`ed.`	Integrated Formal Methods, 5th International Conference, IFM 2005, Eindhoven, The Netherlands, November 29 - December 2, 2005, Proceedings IFM Judi Romijn, Graeme Smith, Jaco van de Pol
2005	—	`conf`	Model Checking Downward Simulations. REFINE Graeme Smith, John Derrick
2005	—	`conf`	Model Checking Z Specifications Using SAL. ZB Graeme Smith, Luke Wildman
2005	—	`conf`	Preface. IFM Doctoral Symposium Judi Romijn, Graeme Smith, Jaco van de Pol
2004	—	`conf`	Architectural Design in Object-Z. Australian Software Engineering Conference Tim McComb, Graeme Smith
2004	B	`ed.`	Integrated Formal Methods, 4th International Conference, IFM 2004, Canterbury, UK, April 4-7, 2004, Proceedings IFM Eerke A. Boiten, John Derrick, Graeme Smith
2004	—	`conf`	Linear Temporal Logic and Z Refinement. AMAST John Derrick, Graeme Smith
2003	B	`conf`	Animation of Object-Z Specifications Using a Z Animator. SEFM Tim McComb, Graeme Smith
2003	—	`conf`	Compositional Verification for Object-Z. ZB Kirsten Winter, Graeme Smith
2003	—	`conf`	Proving Temporal Properties of Z Specifications Using Abstraction. ZB Graeme Smith, Kirsten Winter
2003	J	`jnl`	Structural Refinement of Systems Specified in Object-Z and CSP. Formal Aspects Comput. John Derrick, Graeme Smith
2002	C	`conf`	Abstract Specification in Object-Z and CSP. ICFEM Graeme Smith, John Derrick
2002	B	`conf`	An Integration of Real-Time Object-Z and CSP for Specifying Concurrent Real-Time Systems. IFM Graeme Smith
2002	J	`jnl`	An Introduction to Real-Time Object-Z. Formal Aspects Comput. Graeme Smith, Ian J. Hayes
2002	—	`conf`	Encoding Object-Z in Isabelle/HOL. ZB Graeme Smith, Florian Kammüller, Thomas Santen
2002	C	`conf`	Introducing Reference Semantics via Refinement. ICFEM Graeme Smith
2001	C	`conf`	Model Checking Object-Z Classes: Some Experiments with FDR. APSEC Geoff Kassel, Graeme Smith
2001	J	`jnl`	Specification, Refinement and Verification of Concurrent Systems-An Integration of Object-Z and CSP. Formal Methods Syst. Des. Graeme Smith, John Derrick
2000	J	`jnl`	Incremental Development of Real-Time Requirements: The Light Control Case Study. J. Univers. Comput. Sci. Graeme Smith, Colin J. Fidge
2000	—	`conf`	Stepwise Development from Ideal Specifications. ACSC Graeme Smith
2000	B	`conf`	Structural Refinement in Object-Z/CSP. IFM John Derrick, Graeme Smith
2000	B	`conf`	Structuring Real-Time Object-Z Specifications. IFM Graeme Smith, Ian J. Hayes
1999	B	`conf`	Towards Real-Time Object-Z. IFM Graeme Smith, Ian J. Hayes
1997	—	`conf`	A Semantic Integration of Object-Z and CSP for the Specification of Concurrent Systems. FME Graeme Smith
1997	C	`conf`	Combining CSP and Object-Z: Finite or Infinite Trace Semantics? FORTE Clemens Fischer, Graeme Smith
1997	C	`conf`	Refinement and Verification of Concurrent Systems Specified in Object-Z and CSP. ICFEM Graeme Smith, John Derrick
1996	J	`jnl`	A Blocking Model for Reactive Objects. Formal Aspects Comput. Roger Duke, Cecily Bailes, Graeme Smith
1995	J	`jnl`	A Fully Abstract Semantics of Classes for Object-Z. Formal Aspects Comput. Graeme Smith
1994	C	`conf`	Formal definitions of behavioural compatibility for active and passive objects. APSEC Graeme Smith
1992	—	`—`	An object-oriented approach to formal specification Graeme Smith
1991	—	`conf`	Associated Paper: The Object-Z Specification Language. TOOLS (5) Roger Duke, Paul King, Gordon A. Rose, Graeme Smith
1990	—	`conf`	Formalisation of behavioural and structural concepts for communication systems. PSTV Paul King, Graeme Smith
1990	C	`conf`	Transferring Formal Techniques to Industry. FORTE Roger Duke, Gordon A. Rose, Graeme Smith
1989	C	`conf`	Object-Z: An Object-Oriented Extension to Z. FORTE David A. Carrington, David J. Duke, Roger Duke, Paul King, Gordon A. Rose, Graeme Smith
1989	J	`jnl`	Temporal Logic and Z Specifications. Aust. Comput. J. Roger Duke, Graeme Smith