| 2024 | NCA | Hooks: A Simple and Modular Checkpointing Protocol for Blockchains. | Pedro Antonino, Antoine Durand, Namrata Jain, Garry Lancaster, Jonathan Lawrence, A. W. Roscoe |
| 2023 | ESORICS | Optimally-Fair Multi-party Exchange Without Trusted Parties. | Ivo Maffei, A. W. Roscoe |
| 2022 | SEFM | Specification is Law: Safe Creation and Upgrade of Ethereum Smart Contracts. | Pedro Antonino, Juliandson Ferreira, Augusto Sampaio, A. W. Roscoe |
| 2021 | ACISP | Partially-Fair Computation from Timed-Release Encryption and Oblivious Transfer. | Geoffroy Couteau, A. W. Roscoe, Peter Y. A. Ryan |
| 2021 | SAC | Solidifier: bounded model checking solidity using lazy contract deployment and precise memory modelling. | Pedro Antonino, A. W. Roscoe |
| 2020 | ICISSP | Neural Network Security: Hiding CNN Parameters with Guided Grad-CAM. | Linda Guiga, A. W. Roscoe |
| 2017 | CW | Software and Malware Capabilities: Opinions on (Inter)national Security. | Jantje A. M. Silomon, A. W. Roscoe |
| 2017 | TACAS | The Automatic Detection of Token Structures and Invariants Using SAT Checking. | Pedro R. G. Antonino, Thomas Gibson-Robinson, A. W. Roscoe |
| 2016 | FM | Tighter Reachability Criteria for Deadlock-Freedom Analysis. | Pedro R. G. Antonino, Thomas Gibson-Robinson, A. W. Roscoe |
| 2016 | IFM | Efficient Deadlock-Freedom Checking Using Local Analysis and SAT Solving. | Pedro Antonino, Thomas Gibson-Robinson, A. W. Roscoe |
| 2014 | ICFEM | Computing Maximal Bisimulations. | Alexandre Boulgakov, Thomas Gibson-Robinson, A. W. Roscoe |
| 2014 | TACAS | FDR3 - A Modern Refinement Checker for CSP. | Thomas Gibson-Robinson, Philip J. Armstrong, Alexandre Boulgakov, A. W. Roscoe |
| 2012 | CAV | Recent Developments in FDR. | Philip J. Armstrong, Michael Goldsmith, Gavin Lowe, Jol Ouaknine, Hristina Palikareva, A. W. Roscoe, James Worrell |
| 2012 | FSE | Short-Output Universal Hash Functions and Their Use in Fast and Secure Data Authentication. | Long Hoang Nguyen, A. W. Roscoe |
| 2011 | CONCUR | Static Livelock Analysis in CSP. | Jol Ouaknine, Hristina Palikareva, A. W. Roscoe, James Worrell |
| 2011 | WISTP | Mobile Electronic Identity: Securing Payment on Mobile Phones. | Chen Bangdao, A. W. Roscoe |
| 2010 | IWSEC | The Missing Link: Human Interactive Security Protocols in Mobile Payment. | Chen Bangdao, A. W. Roscoe, Ronald Kainda, Long Hoang Nguyen |
| 2010 | SOUPS | Two heads are better than one: security and usability of device associations in group scenarios. | Ronald Kainda, Ivan Flechais, A. W. Roscoe |
| 2010 | WISTP | Secure and Usable Out-Of-Band Channels for | Ronald Kainda, Ivan Flechais, A. W. Roscoe |
| 2009 | ATVA | Local Search in Model Checking. | A. W. Roscoe, Philip J. Armstrong, Pragyesh |
| 2009 | SOUPS | Usability and security of out-of-band channels in secure device pairing protocols. | Ronald Kainda, Ivan Flechais, A. W. Roscoe |
| 2008 | ICTAC | The Three Platonic Models of Divergence-Strict CSP. | A. W. Roscoe |
| 2006 | ICFEM | Verifying Statemate Statecharts Using CSP and FDR. | A. W. Roscoe, Zhenzhong Wu |
| 2006 | SAC | Extending noninterference properties to the timed world. | Jian Huang, A. W. Roscoe |
| 2004 | IFM | Relating Data Independent Trace Checks in CSP with UNITY Reachability under a Normality Assumption. | Xu Wang, A. W. Roscoe, Ranko Lazic |
| 2000 | ESORICS | Automating Data Independence. | Philippa J. Broadfoot, Gavin Lowe, A. W. Roscoe |
| 2000 | PDPTA | Data Independent Induction over Structured Networks. | S. J. Creese, A. W. Roscoe |
| 1999 | FORTE | Verifying an infinite family of inductions simultaneously using data independence and FDR. | S. J. Creese, A. W. Roscoe |
| 1999 | PDPTA | Formal Verification of Arbitrary Network Topologies. | S. J. Creese, A. W. Roscoe |
| 1995 | SP | CSP and determinism in security modelling. | A. W. Roscoe |
| 1995 | TACAS | Hierarchical Compression for Model-Checking CSP or How to Check 10 | A. W. Roscoe, Paul H. B. Gardiner, Michael Goldsmith, J. R. Hulance, D. M. Jackson, J. Bryan Scattergood |
| 1994 | ESORICS | Non-Interference Through Determinism. | A. W. Roscoe, Jim Woodcock, Lars Wulf |
| 1989 | CONCUR | Analysing | George M. Reed, A. W. Roscoe |
| 1989 | MFPS | Unbounded Nondeterminism in CSP. | A. W. Roscoe, Geoff Barrett |
| 1987 | MFPS | Metric Spaces as Models for Real-Time Concurrency. | George M. Reed, A. W. Roscoe |
| 1986 | ICALP | A Timed Model for Communicating Sequential Processes. | George M. Reed, A. W. Roscoe |
| 1984 | CONCUR | An Improved Failures Model for Communicating Processes. | Stephen D. Brookes, A. W. Roscoe |
| 1984 | CONCUR | Denotational Semantics for occam. | A. W. Roscoe |