| 2022 | ICECCS | Denotational and Algebraic Semantics for Cyber-physical Systems. | Ran Li, Huibiao Zhu, Richard Banach |
| 2022 | ICFEM | A Proof System for Cyber-Physical Systems with Shared-Variable Concurrency. | Ran Li, Huibiao Zhu, Richard Banach |
| 2022 | SETTA | Translating CPS with Shared-Variable Concurrency in SpaceEx. | Ran Li, Huibiao Zhu, Richard Banach |
| 2019 | FC | Verification-Led Smart Contracts. | Richard Banach |
| 2019 | FM | Formal Modelling and Verification as Rigorous Review Technology: An Inspiration from INSPEX. | Richard Banach, Joseph Razavi, Olivier Debicki, Suzanne Lesecq |
| 2018 | FedCSIS | Assistive Smart, Structured 3D Environmental Information for the Visually Impaired and Blind: Leveraging the INSPEX Concept. | Suzanne Lesecq, Olivier Debicki, Laurent Ouvry, Christian Fabre, Nicolas Mareau, Julie Foucault, Francois Birot, Loc Sevrin, Steve Buckley, Carl Jackson, John Barrett, Alan McGibney, Susan Rea, David Rojas, Richard Banach, Joseph Razavi, Marc Correvon, Gabriela Dudnik, Jean-Marc Van Gyseghem, Jean Herveg, Nathalie Grandjean, Florence Thiry, Cian O'Murchu, Alan Mathewson, Rosemary O'Keeffe, Andrea Di Matteo, Vincenza Di Palma, Fabio Quaglia, Giuseppe Villa |
| 2018 | ICSoft | Formal Verification for Advanced Sensing Applications: Data Pre-processing in the INSPEX System. | Joseph Razavi, Richard Banach, Suzanne Lesecq, Olivier Debicki, Nicolas Mareau, Julie Foucault, Marc Correvon, Gabriela Dudnik |
| 2017 | DATE | INSPEX: Design and integration of a portable/wearable smart spatial exploration system. | Suzanne Lesecq, Julie Foucault, Francois Birot, Hugues de Chaumont, Carl Jackson, Marc Correvon, P. Heck, Richard Banach, Andrea Di Matteo, Vincenza Di Palma, John Barrett, Susan Rea, Jean-Marc Van Gyseghem, Cian O'Murchu, Alan Mathewson |
| 2016 | ICFEM | Modelling Hybrid Systems in Event-B and Hybrid Event-B: A Comparison of Water Tanks. | Richard Banach, Michael J. Butler |
| 2016 | TASE | Formal Refinement and Partitioning of a Fuel Pump System for Small Aircraft in Hybrid Event-B. | Richard Banach |
| 2015 | ENASE | Stochastic Analogues of Invariants - Martingales in Stochastic Event-B. | Richard Banach |
| 2015 | FedCSIS | Simulation and formal modelling of yaw control in a drive-by-wire application. | Richard Banach, Pieter Van Schaik, Eric Verhulst |
| 2014 | TASE | Contemplating the Addition of Stochastic Behaviour to Hybrid Event-B. | Richard Banach |
| 2013 | ICTAC | Cruise Control in Hybrid Event-B. | Richard Banach, Michael J. Butler |
| 2010 | SAC | A deidealisation semantics for KAOS. | Richard Banach |
| 2009 | TASE | Coarse Grained Retrenchment and the Mondex Denial of Service Attacks. | Richard Banach |
| 2007 | SEFM | Retrenchment and the Atomicity Pattern. | Richard Banach, Czeslaw Jeske, Anthony Hall, Susan Stepney |
| 2007 | SEFM | Configurable Proof Obligations in the Frog Toolkit. | Simon Fraser, Richard Banach |
| 2006 | ISoLA | Retrenching the Purse: Hashing Injective CLEAR Codes, and Security Properties. | Richard Banach, Michael Poppleton, Czeslaw Jeske, Susan Stepney |
| 2006 | SAFECOMP | Retrenchment, and the Generation of Fault Trees for Static, Dynamic and Cyclic Systems. | Richard Banach, Marco Bozzano |
| 2006 | SEFM | Retrenchment Tutorial. | Richard Banach |
| 2006 | SEFM | Filtering Retrenchments into Refinements. | Richard Banach, John Derrick |
| 2006 | SEW | Retrenching the Purse: Finite Exception Logs, and Validating the Small. | Richard Banach, Michael Poppleton, Susan Stepney |
| 2005 | FM | Retrenching the Purse: Finite Sequence Numbers, and the Tower Pattern. | Richard Banach, Michael Poppleton, Czeslaw Jeske, Susan Stepney |
| 2004 | ICECCS | Requirements Validation by Lifting Retrenchments in B. | Michael Poppleton, Richard Banach |
| 2004 | SAFECOMP | Safety Requirements and Fault Trees Using Retrenchment. | Richard Banach, R. Cross |
| 2003 | FM | Structuring Retrenchments in B by Decomposition. | Michael Poppleton, Richard Banach |
| 2002 | IFM | Minimally and Maximally Abstract Retrenchments. | Czeslaw Jeske, Richard Banach |
| 2000 | ICFEM | Maximally Abstract Retrenchments. | Richard Banach |
| 2000 | ICFEM | Fragmented Retrenchment, Concurrency and Fairness. | Richard Banach, Michael Poppleton |
| 1999 | FM | Retrenchment. | Richard Banach, Michael Poppleton |
| 1999 | IFM | Retrenchment and Punctured Simulation. | Richard Banach, Michael Poppleton |
| 1997 | SAC | Implementing interaction nets in MONSTR. | Richard Banach, George A. Papadopoulos |
| 1995 | SAC | Linear behaviour of term graph rewriting programs. | Richard Banach, George A. Papadopoulos |
| 1988 | ISCA | Flagship: A Parallel Architecture for Declarative Programming. | Ian Watson, Viv Woods, Paul Watson, Richard Banach, Mark Irvine Greenberg, John Sargeant |