Flagship: A Parallel Architecture for Declarative Programming. - Ian Watson; Viv Woods; Paul Watson 001; Richard Banach; Mark Irvine Greenberg; John Sargeant (ISCA, 1988)

Dataflow Analysis of Term Graph Rewriting Systems. - Richard Banach (PARLE (2), 1989)

Simple Type Inference for Term Graph Rewriting Systems. - Richard Banach (CTRS, 1992)

The Contractum in Algebraic Graph Rewriting. - Richard Banach (TAGT, 1994)

Regular Relations and Bicartesian Squares. - Richard Banach (Theor. Comput. Sci., 1994)

Term Graph Rewriting and Garbage Collection Using Ppfibrations. - Richard Banach (Theor. Comput. Sci., 1994)

Linear behaviour of term graph rewriting programs. - Richard Banach; George A. Papadopoulos (SAC, 1995)

Sequent Reconstruction in LLM - A Sweepline Proof. - Richard Banach (Ann. Pure Appl. Log., 1995)

DPO rewriting and abstract semantics via opfibrations. - Richard Banach (SEGRAGRA, 1995)

A Translation of the Pi-Caculus Into MONSTR. - Richard Banach; J. Balazs; G. Papadoupolous (J. Univers. Comput. Sci., 1995)

On Regularity in Software Design. - Richard Banach (Sci. Comput. Program., 1995)

Locating the Contractum in the Double Pushout Approach. - Richard Banach (Theor. Comput. Sci., 1995)

Transitive Term Graph Rewriting. - Richard Banach (Inf. Process. Lett., 1996)

MONSTR I - Fundamental Issues and the Design of MONSTR. - Richard Banach (J. Univers. Comput. Sci., 1996)

Implementing interaction nets in MONSTR. - Richard Banach; George A. Papadopoulos (SAC, 1997)

A study of two graph rewriting formalisms: Interaction Nets and MONSTR. - Richard Banach; George A. Papadopoulos (J. Program. Lang., 1997)

MONSTR II - Suspending Semantics and Independence. - Richard Banach (J. Univers. Comput. Sci., 1997)

MONSTR V - Transitive Coercing Semantics and the Church-Rosser Property. - Richard Banach (J. Univers. Comput. Sci., 1997)

Retrenchment: An Engineering Variation on Refinement. - Richard Banach; Michael Poppleton (B, 1998)

Retrenchment. - Richard Banach; Michael Poppleton (World Congress on Formal Methods, 1999)

Retrenchment and Punctured Simulation. - Richard Banach; Michael Poppleton (IFM, 1999)

Retrenchment: Extending the Reach of Refinement. - Michael Poppleton; Richard Banach (ASE, 1999)

Sharp Retrenchment, Modulated Refinement and Simulation. - Richard Banach; Michael Poppleton (Formal Aspects Comput., 1999)

Maximally Abstract Retrenchments. - Richard Banach (ICFEM, 2000)

Fragmented Retrenchment, Concurrency and Fairness. - Richard Banach; Michael Poppleton (ICFEM, 2000)

Retrenchment: Extending Refinement for Continuous and Control Systems. - Michael Poppleton; Richard Banach (IWFM, 2000)

Retrenchment, Refinement, and Simulation. - Richard Banach; Michael Poppleton (ZB, 2000)

Minimally and Maximally Abstract Retrenchments. - Czeslaw Jeske; Richard Banach (IFM, 2002)

Controlling Control Systems: An Application of Evolving Retrenchment. - Michael Poppleton; Richard Banach (ZB, 2002)

IWIM Semantics via Fibred Automata. - Richard Banach; Farhad Arbab; George A. Papadopoulos; John R. W. Glauert (Formal Methods and Component Interaction @ ICALP, 2002)

Book Reviews. - Richard Banach (Softw. Test. Verification Reliab., 2002)

Structuring Retrenchments in B by Decomposition. - Michael Poppleton; Richard Banach (FME, 2003)

A Multiply Hierarchical Automaton Semantics for the IWIM Coordination Model. - Richard Banach; Farhad Arbab; George A. Papadopoulos; John R. W. Glauert (J. Univers. Comput. Sci., 2003)

Book Review: "Refinement in Z and object-Z: Foundations and Advanced Applications" by John Derrick and Eerke Boiten. - Richard Banach (J. Log. Comput., 2003)

Book Review: "Concurrency Verification: Introduction to Compositional and Non-compositional Methods" by Willem-Paul de Roever, Frank de Boer, Ulrich Hanneman, Jozef Hooman, Yassine Lakhnech, Mannes Poel and Job Zwiers (eds.). - Richard Banach (J. Log. Comput., 2003)

Review: Mathematics of Quantum Computation. - Richard Banach (J. Log. Comput., 2003)

Review: Handbook of Process Algebra. - Richard Banach (J. Log. Comput., 2003)

Retrenching partial requirements into system definitions: a simple feature interaction case study. - Richard Banach; Michael Poppleton (Requir. Eng., 2003)

Requirements Validation by Lifting Retrenchments in B. - Michael Poppleton; Richard Banach (ICECCS, 2004)

Safety Requirements and Fault Trees Using Retrenchment. - Richard Banach; R. Cross (SAFECOMP, 2004)

Review: Process Algebra with Timing. - Richard Banach (J. Log. Comput., 2004)

Retrenchment and the Mondex Electronic Purse. - Richard Banach; Michael Poppleton; Czeslaw Jeske; Susan Stepney (Abstract State Machines, 2005)

Retrenching the Purse: Finite Sequence Numbers, and the Tower Pattern. - Richard Banach; Michael Poppleton; Czeslaw Jeske; Susan Stepney (FM, 2005)

Retrenchment and the B-Toolkit. - Richard Banach; Simon Fraser (ZB, 2005)

Retrenching the Purse: Hashing Injective CLEAR Codes, and Security Properties. - Richard Banach; Michael Poppleton; Czeslaw Jeske; Susan Stepney (ISoLA, 2006)

Retrenchment, and the Generation of Fault Trees for Static, Dynamic and Cyclic Systems. - Richard Banach; Marco Bozzano (SAFECOMP, 2006)

Retrenchment Tutorial. - Richard Banach (SEFM, 2006)

Filtering Retrenchments into Refinements. - Richard Banach; John Derrick (SEFM, 2006)

Retrenching the Purse: Finite Exception Logs, and Validating the Small. - Richard Banach; Michael Poppleton; Susan Stepney (SEW, 2006)

Retrenchment and the Atomicity Pattern. - Richard Banach; Czeslaw Jeske; Anthony Hall; Susan Stepney (SEFM, 2007)

Configurable Proof Obligations in the Frog Toolkit. - Simon Fraser; Richard Banach (SEFM, 2007)

On the Refinement of Atomic Actions. - Richard Banach; Gerhard Schellhorn (REFINE@IFM, 2007)

Retrenching the Purse: The Balance Enquiry Quandary, and Generalised and (1, 1) Forward Refinements. - Richard Banach; Czeslaw Jeske; Michael Poppleton; Susan Stepney (Fundam. Informaticae, 2007)

Formal Methods Guest Editorial. - Richard Banach (J. Univers. Comput. Sci., 2007)

The Verification Grand Challenge. - Jim Woodcock 001; Richard Banach (J. Univers. Comput. Sci., 2007)

Engineering and theoretical underpinnings of retrenchment. - Richard Banach; Michael Poppleton; Czeslaw Jeske; Susan Stepney (Sci. Comput. Program., 2007)

Model Based Refinement and the Tools of Tomorrow. - Richard Banach (ABZ, 2008)

UseCase-Wise Development: Retrenchment for Event-B. - Richard Banach (ABZ, 2008)

A Concept-Driven Construction of the Mondex Protocol Using Three Refinements. - Gerhard Schellhorn; Richard Banach (ABZ, 2008)

Composition mechanisms for retrenchment. - Richard Banach; Czeslaw Jeske; Michael Poppleton (J. Log. Algebraic Methods Program., 2008)

Coarse Grained Retrenchment and the Mondex Denial of Service Attacks. - Richard Banach (TASE, 2009)

A deidealisation semantics for KAOS. - Richard Banach (SAC, 2010)

Atomic actions, and their refinements to isolated protocols. - Richard Banach; Gerhard Schellhorn (Formal Aspects Comput., 2010)

Stronger compositions for retrenchments. - Richard Banach; Czeslaw Jeske (J. Log. Algebraic Methods Program., 2010)

Formalising the Continuous/Discrete Modeling Step - Richard Banach; Huibiao Zhu; Wen Su; Runlei Huang (Refine@FM, 2011)

Retrenchment for Event-B: UseCase-wise development and Rodin integration. - Richard Banach (Formal Aspects Comput., 2011)

Simple feature engineering via neat default retrenchments. - Richard Banach; Czeslaw Jeske (J. Log. Algebraic Methods Program., 2011)

Review of Modeling in Event-B: System and Sofware Engineering, 1st edition, by Jean-Raymond Abrial. - Richard Banach (J. Log. Comput., 2011)

ASM and Controller Synthesis. - Richard Banach; Huibiao Zhu; Wen Su; Xiaofeng Wu (ABZ, 2012)

Continuous ASM, and a Pacemaker Sensing Fragment. - Richard Banach; Huibiao Zhu; Wen Su; Xiaofeng Wu (ABZ, 2012)

Continuous Behaviour in Event-B: A Sketch. - Richard Banach; Huibiao Zhu; Wen Su; Xiaofeng Wu (ABZ, 2012)

Pliant Modalities in Hybrid Event-B. - Richard Banach (Theories of Programming and Formal Methods, 2013)

A Hybrid Event-B Study of Lane Centering. - Richard Banach; Michael J. Butler (CSDM, 2013)

Cruise Control in Hybrid Event-B. - Richard Banach; Michael J. Butler (ICTAC, 2013)

The mechanical generation of fault trees for reactive systems via retrenchment I: combinational circuits. - Richard Banach; Marco Bozzano (Formal Aspects Comput., 2013)

The mechanical generation of fault trees for reactive systems via retrenchment II: clocked and feedback circuits. - Richard Banach; Marco Bozzano (Formal Aspects Comput., 2013)

Atomicity failure and the retrenchment atomicity pattern. - Richard Banach; Czeslaw Jeske; Anthony Hall; Susan Stepney (Formal Aspects Comput., 2013)

Invariant Guided System Decomposition. - Richard Banach (ABZ, 2014)

The Landing Gear Case Study in Hybrid Event-B. - Richard Banach (ABZ (Case Study), 2014)

Contemplating the Addition of Stochastic Behaviour to Hybrid Event-B. - Richard Banach (TASE, 2014)

Continuous KAOS, ASM, and formal control system design across the continuous/discrete modeling interface: a simple train stopping application. - Richard Banach; Huibiao Zhu; Wen Su; Runlei Huang (Formal Aspects Comput., 2014)

ASM, controller synthesis, and complete refinement. - Richard Banach; Huibiao Zhu; Wen Su; Xiaofeng Wu (Sci. Comput. Program., 2014)

A Continuous ASM Modelling Approach to Pacemaker Sensing. - Richard Banach; Huibiao Zhu; Wen Su; Xiaofeng Wu (ACM Trans. Softw. Eng. Methodol., 2014)

Stochastic Analogues of Invariants - Martingales in Stochastic Event-B. - Richard Banach (ENASE, 2015)

Simulation and formal modelling of yaw control in a drive-by-wire application. - Richard Banach; Pieter Van Schaik; Eric Verhulst (FedCSIS, 2015)

Retrenchment and refinement interworking: the tower theorems. - Richard Banach; Czeslaw Jeske (Math. Struct. Comput. Sci., 2015)

Core Hybrid Event-B I: Single Hybrid Event-B machines. - Richard Banach; Michael J. Butler; Shengchao Qin; Nitika Verma; Huibiao Zhu (Sci. Comput. Program., 2015)

Modelling and Refining Hybrid Systems in Event-B and Rodin. - Michael J. Butler; Jean-Raymond Abrial; Richard Banach (From Action Systems to Distributed Systems, 2016)

Hemodialysis Machine in Hybrid Event-B. - Richard Banach (ABZ, 2016)

Shared-Variable Concurrency, Continuous Behaviour and Healthiness for Critical Cyberphysical Systems. - Richard Banach; Huibiao Zhu (FTSCS, 2016)

Modelling Hybrid Systems in Event-B and Hybrid Event-B: A Comparison of Water Tanks. - Richard Banach; Michael J. Butler (ICFEM, 2016)

Formal Refinement and Partitioning of a Fuel Pump System for Small Aircraft in Hybrid Event-B. - Richard Banach (TASE, 2016)

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; et al. (DATE, 2017)

Invariant Management in the Presence of Failures. - Richard Banach (IMBSA, 2017)

Core Hybrid Event-B II: Multiple cooperating Hybrid Event-B machines. - Richard Banach; Michael J. Butler; Shengchao Qin; Huibiao Zhu (Sci. Comput. Program., 2017)

The landing gear system in multi-machine Hybrid Event-B. - Richard Banach (Int. J. Softw. Tools Technol. Transf., 2017)

Issues in Automated Urban Train Control: 'Tackling' the Rugby Club Problem. - Richard Banach (ABZ, 2018)

Cyberphysical Systems: A Behind-the-Scenes Foundational View. - Richard Banach; Wen Su (Models: Concepts, Theory, Logic, Reasoning and Semantics, 2018)

Formal Methods in Systems Integration: Deployment of Formal Techniques in INSPEX. - Richard Banach; Joe Razavi; Suzanne Lesecq; Olivier Debicki; Nicolas Mareau; Julie Foucault; Marc Correvon; Gabriela Dudnik (CSDM, 2018)

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; Loïc Sevrin; Steve Buckley; Carl Jackson; John Barrett; Alan McGibney; et al. (FedCSIS (Communication Papers), 2018)

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 (ICSOFT, 2018)

Exploring Applications of Formal Methods in the INSPEX Project. - Joseph Razavi; Richard Banach; Olivier Debicki; Nicolas Mareau; Suzanne Lesecq; Julie Foucault (STAF Workshops, 2018)

Modelling, formal refinement and partitioning strategies for a small aircraft fuel pump system in Hybrid Event-B. - Richard Banach (Sci. Comput. Program., 2018)

Verification-Led Smart Contracts. - Richard Banach (Financial Cryptography Workshops, 2019)

Formal Modelling and Verification as Rigorous Review Technology: An Inspiration from INSPEX. - Richard Banach; Joseph Razavi; Olivier Debicki; Suzanne Lesecq (FM Workshops (1), 2019)

Punishment not Reward: Disincentivising Blockchain Application Misbehaviour. - Richard Banach (IEEE ICBC, 2019)

John Fitzgerald, Peter Gorm Larsen, Marcel Verhoef (eds): Collaborative design for embedded systems - Springer, Berlin Heidelberg, 2014. - Richard Banach (Formal Aspects Comput., 2019)

INSPEX: Optimize Range Sensors for Environment Perception as a Portable System. - Julie Foucault; Suzanne Lesecq; Gabriela Dudnik; Marc Correvon; Rosemary O'Keeffe; Vincenza Di Palma; Marco Passoni; Fabio Quaglia; Laurent Ouvry; Steve Buckley; Jean Herveg; Andrea Di Matteo; et al. (Sensors, 2019)

Automated urban train control with hybrid Event-B: 'Tackling' the rugby club problem. - Richard Banach (Sci. Comput. Program., 2020)

Moded and Continuous Abstract State Machines. - Richard Banach; Huibiao Zhu (Logic, Computation and Rigorous Methods, 2021)

Blockchain applications beyond the cryptocurrency casino: The Punishment not Reward blockchain architecture. - Richard Banach (Concurr. Comput. Pract. Exp., 2021)

Formal methods by stealth: The INSPEX experience. - Richard Banach; Joseph Razavi; Olivier Debicki; Suzanne Lesecq (J. Softw. Evol. Process., 2021)

Language evolution and healthiness for critical cyber-physical systems. - Richard Banach; Huibiao Zhu (J. Softw. Evol. Process., 2021)

Denotational and Algebraic Semantics for Cyber-physical Systems. - Ran Li; Huibiao Zhu; Richard Banach (ICECCS, 2022)

A Proof System for Cyber-Physical Systems with Shared-Variable Concurrency. - Ran Li; Huibiao Zhu; Richard Banach (ICFEM, 2022)

Translating CPS with Shared-Variable Concurrency in SpaceEx. - Ran Li; Huibiao Zhu; Richard Banach (SETTA, 2022)

Formalisation, Abstraction and Refinement of Bond Graphs. - Richard Banach; John W. Baugh Jr. (ICGT, 2023)

Exploring the Privacy Concerns in Permissionless Blockchain Networks and Potential Solutions. - Talgar Bayan; Richard Banach (CoRR, 2023)

Graded Refinement, Retrenchment, and Simulation. - Richard Banach (ACM Trans. Softw. Eng. Methodol., 2023)

Translating and verifying Cyber-Physical systems with shared-variable concurrency in SpaceEx. - Ran Li; Huibiao Zhu; Richard Banach (Internet Things, 2023)

The 'Causality' Quagmire for Formalised Bond Graphs. - Richard Banach; John W. Baugh Jr. (ICGT, 2024)

A Privacy-Preserving DAO Model Using NFT Authentication for the Punishment not Reward Blockchain Architecture. - Talgar Bayan; Richard Banach (CoRR, 2024)

Blockchain-enhanced Integrity Verification in Educational Content Assessment Platform: A Lightweight and Cost-Efficient Approach. - Talgar Bayan; Richard Banach; Askar Nurbekov; Makhmud Mustafabek Galy; Adi Sabyrbayev; Zhanat Nurbekova (CoRR, 2024)

Autonomous System Safety Properties with Multi-Machine Hybrid Event-B. - Richard Banach (FMAS@iFM, 2024)

An algebraic approach to simulation and verification for cyber-physical systems with shared-variable concurrency. - Ran Li; Huibiao Zhu; Richard Banach (J. Log. Algebraic Methods Program., 2024)

Core Hybrid Event-B III: Fundamentals of a reasoning framework. - Richard Banach (Sci. Comput. Program., 2024)