Formal Verification of a Practical Lock-Free Queue Algorithm. - Simon Doherty; Lindsay Groves; Victor Luchangco; Mark Moir (FORTE, 2004)

Bringing practical lock-free synchronization to 64-bit applications. - Simon Doherty; Maurice Herlihy; Victor Luchangco; Mark Moir (PODC, 2004)

DCAS is not a silver bullet for nonblocking algorithm design. - Simon Doherty; David Detlefs; Lindsay Groves; Christine H. Flood; Victor Luchangco; Paul Alan Martin; Mark Moir; Nir Shavit; Guy L. Steele Jr. (SPAA, 2004)

Verifying Concurrent Data Structures by Simulation. - Robert Colvin; Simon Doherty; Lindsay Groves (REFINE, 2005)

Nonblocking Algorithms and Backward Simulation. - Simon Doherty; Mark Moir (DISC, 2009)

Simpler Backward Simulation Proofs. - Simon Doherty; Lindsay Groves (CATS, 2010)

Towards formally specifying and verifying transactional memory. - Simon Doherty; Lindsay Groves; Victor Luchangco; Mark Moir (Formal Aspects Comput., 2013)

Proving Opacity of a Pessimistic STM. - Simon Doherty; Brijesh Dongol; John Derrick; Gerhard Schellhorn; Heike Wehrheim (OPODIS, 2016)

Linearizability and Causality. - Simon Doherty; John Derrick (SEFM, 2016)

Reducing Opacity to Linearizability: A Sound and Complete Method. - Alasdair Armstrong; Brijesh Dongol; Simon Doherty (CoRR, 2016)

Causal Linearizability. - Simon Doherty; John Derrick (CoRR, 2016)

Proving Opacity via Linearizability: A Sound and Complete Method. - Alasdair Armstrong; Brijesh Dongol; Simon Doherty (FORTE, 2017)

Making Linearizability Compositional for Partially Ordered Executions. - Simon Doherty; Brijesh Dongol; Heike Wehrheim; John Derrick (IFM, 2018)

Brief Announcement: Generalising Concurrent Correctness to Weak Memory. - Simon Doherty; Brijesh Dongol; Heike Wehrheim; John Derrick (DISC, 2018)

Causal Linearizability: Compositionality for Partially Ordered Executions. - Simon Doherty; John Derrick; Brijesh Dongol; Heike Wehrheim (CoRR, 2018)

Mechanized proofs of opacity: a comparison of two techniques. - John Derrick; Simon Doherty; Brijesh Dongol; Gerhard Schellhorn; Oleg Travkin; Heike Wehrheim (Formal Aspects Comput., 2018)

Verifying Correctness of Persistent Concurrent Data Structures. - John Derrick; Simon Doherty; Brijesh Dongol; Gerhard Schellhorn; Heike Wehrheim (FM, 2019)

Verifying C11 programs operationally. - Simon Doherty; Brijesh Dongol; Heike Wehrheim; John Derrick (PPoPP, 2019)

Owicki-Gries Reasoning for C11 RAR. - Sadegh Dalvandi; Simon Doherty; Brijesh Dongol; Heike Wehrheim (ECOOP, 2020)

Defining and Verifying Durable Opacity: Correctness for Persistent Software Transactional Memory. - Eleni Bila; Simon Doherty; Brijesh Dongol; John Derrick; Gerhard Schellhorn; Heike Wehrheim (FORTE, 2020)

Relational Semigroups and Object-Free Categories. - James Cranch; Simon Doherty; Georg Struth (CoRR, 2020)

Integrating Owicki-Gries for C11-Style Memory Models into Isabelle/HOL. - Sadegh Dalvandi; Brijesh Dongol; Simon Doherty (CoRR, 2020)

Owicki-Gries Reasoning for C11 RAR (Artifact). - Sadegh Dalvandi; Simon Doherty; Brijesh Dongol; Heike Wehrheim (Dagstuhl Artifacts Ser., 2020)

Brief Announcement: On Strong Observational Refinement and Forward Simulation. - John Derrick; Simon Doherty; Brijesh Dongol; Gerhard Schellhorn; Heike Wehrheim (DISC, 2021)

On Strong Observational Refinement and Forward Simulation. - John Derrick; Simon Doherty; Brijesh Dongol; Gerhard Schellhorn; Heike Wehrheim (CoRR, 2021)

Verifying correctness of persistent concurrent data structures: a sound and complete method. - John Derrick; Simon Doherty; Brijesh Dongol; Gerhard Schellhorn; Heike Wehrheim (Formal Aspects Comput., 2021)

Convolution and concurrency. - James Cranch; Simon Doherty; Georg Struth (Math. Struct. Comput. Sci., 2021)

Integrating Owicki-Gries for C11-Style Memory Models into Isabelle/HOL. - Sadegh Dalvandi; Brijesh Dongol; Simon Doherty; Heike Wehrheim (J. Autom. Reason., 2022)

Modularising Verification Of Durable Opacity. - Eleni Bila; John Derrick; Simon Doherty; Brijesh Dongol; Gerhard Schellhorn; Heike Wehrheim (Log. Methods Comput. Sci., 2022)

Unifying Operational Weak Memory Verification: An Axiomatic Approach. - Simon Doherty; Sadegh Dalvandi; Brijesh Dongol; Heike Wehrheim (ACM Trans. Comput. Log., 2022)