Formal verification of a practical lock-free queue algorithm S Doherty, L Groves, V Luchangco, M Moir Formal Techniques for Networked and Distributed Systems–FORTE 2004: 24th …, 2004 | 148 | 2004 |
DCAS is not a silver bullet for nonblocking algorithm design S Doherty, DL Detlefs, L Groves, CH Flood, V Luchangco, PA Martin, ... Proceedings of the sixteenth annual ACM symposium on Parallelism in …, 2004 | 106 | 2004 |
Towards formally specifying and verifying transactional memory S Doherty, L Groves, V Luchangco, M Moir Formal Aspects of Computing 25 (5), 769-799, 2013 | 104 | 2013 |
Verifying concurrent data structures by simulation R Colvin, S Doherty, L Groves Electronic Notes in Theoretical Computer Science 137 (2), 93-110, 2005 | 54 | 2005 |
Verifying C11 programs operationally S Doherty, B Dongol, H Wehrheim, J Derrick Proceedings of the 24th Symposium on Principles and Practice of Parallel …, 2019 | 48 | 2019 |
Bringing practical lock-free synchronization to 64-bit applications S Doherty, M Herlihy, V Luchangco, M Moir Proceedings of the twenty-third annual ACM symposium on Principles of …, 2004 | 43 | 2004 |
Towards formally specifying and verifying transactional memory S Doherty, L Groves, V Luchangco, M Moir Electronic Notes in Theoretical Computer Science 259, 245-261, 2009 | 36 | 2009 |
Owicki-Gries reasoning for C11 RAR S Dalvandi, S Doherty, B Dongol, H Wehrheim 34th European Conference on Object-Oriented Programming (ECOOP 2020), 2020 | 34 | 2020 |
Modelling and verifying non-blocking algorithms that use dynamically allocated memory S Doherty Victoria University of Wellington, 2003 | 30 | 2003 |
Integrating Owicki–Gries for C11-style memory models into Isabelle/HOL S Dalvandi, B Dongol, S Doherty, H Wehrheim Journal of Automated Reasoning 66 (1), 141-171, 2022 | 23 | 2022 |
Making linearizability compositional for partially ordered executions S Doherty, B Dongol, H Wehrheim, J Derrick Integrated Formal Methods: 14th International Conference, IFM 2018, Maynooth …, 2018 | 23 | 2018 |
Verifying correctness of persistent concurrent data structures J Derrick, S Doherty, B Dongol, G Schellhorn, H Wehrheim International Symposium on Formal Methods, 179-195, 2019 | 18 | 2019 |
Proving opacity of a pessimistic STM S Doherty, B Dongol, J Derrick, G Schellhorn, H Wehrheim Leibniz International Proceedings in Informatics 70 (35), 35.1-35.17, 2017 | 17 | 2017 |
Code preparation technique employing lock-free pointer operations MS Moir, DL Detlefs, S Doherty, MP Herlihy, VM Luchangco, PA Martin, ... US Patent 7,805,467, 2010 | 16 | 2010 |
Lightweight reference counting using single-target synchronization S Doherty, MP Herlihy, VM Luchangco, MS Moir US Patent 7,769,791, 2010 | 14 | 2010 |
Nonblocking algorithms and backward simulation S Doherty, M Moir International Symposium on Distributed Computing, 274-288, 2009 | 14 | 2009 |
Unifying operational weak memory verification: an axiomatic approach S Doherty, S Dalvandi, B Dongol, H Wehrheim ACM Transactions on Computational Logic 23 (4), 1-39, 2022 | 13 | 2022 |
Proving opacity via linearizability: a sound and complete method A Armstrong, B Dongol, S Doherty Formal Techniques for Distributed Objects, Components, and Systems: 37th …, 2017 | 13 | 2017 |
Defining and verifying durable opacity: Correctness for persistent software transactional memory E Bila, S Doherty, B Dongol, J Derrick, G Schellhorn, H Wehrheim International Conference on Formal Techniques for Distributed Objects …, 2020 | 12 | 2020 |
Mechanized proofs of opacity: a comparison of two techniques J Derrick, S Doherty, B Dongol, G Schellhorn, O Travkin, H Wehrheim Formal Aspects of Computing 30, 597-625, 2018 | 12 | 2018 |