Most of these are held in the directory http://www.cs.man.ac.uk/~banach/some.pubs (referred to below as . . .) in both ps.gz and pdf forms.
Note that the ps.gz and pdf forms can differ slightly in inessential formatting detail due to the pdf having been produced using later releases of the document processing software in some cases, and/or ps2pdf vagaries.
Last Updated: 23.04.24
Academic Journal Papers R. Li, H. Zhu, R. Banach 2024 J. Log. Alg. Meth. Prog., 25pp., to appear, `An Algebraic Approach to Simulation and Verification for Cyber-Physical Systems with Shared-Variable Concurrency' Preprint: .../AlgAppSimVerCPS.ps.gz .../AlgAppSimVerCPS.pdf R. Banach 2024 Sci. Comp. Prog., 231, 103002, 54pp., `Core Hybrid Event-B III: Fundamentals of a Reasoning Framework.' Preprint: .../ContEvB--III.ps.gz .../ContEvB--III.pdf R. Li, H. Zhu, R. Banach 2023 J. Internet of Things, 23, 100864, 18pp., `Translating and Verifying Cyber-Physical Systems with Shared-Variable Concurrency in SpaceEx' Preprint: .../TranVerCPSSpace.ps.gz .../TranVerCPSSpace.pdf R. Banach 2023 ACM Trans. Soft. Eng. Meth., 32, 1-69, `Graded Refinement, Retrenchment and Simulation' Preprint: .../GradedRetRefSim.ps.gz .../GradedRetRefSim.pdf R. Banach, J. Razavi, O. Debicki, S. Lesecq 2021 J. Soft. Evol. Proc., 33, 2021;e2383, 26pp., `Formal Methods by Stealth: The INSPEX Experience' Preprint: .../INSPEX-JSEP-21.ps.gz .../INSPEX-JSEP-21.pdf R. Banach, H. Zhu 2021 J. Soft. Evol. Proc., 33, 2020;e2301, 24pp., `Language Evolution and Healthiness for Critical Cyber-Physical Systems' Preprint: .../CritCPS.HLTH.ps.gz .../CritCPS.HLTH.pdf R. Banach 2021 Conc. and Comp. Prac. and Exp., 33, 2020;e5749, 27pp., `Blockchain Applications Beyond the Cryptocurrency Casino: The Punishment not Reward (PnR) Blockchain Architecture' Preprint: .../PunRewLONG.ps.gz .../PunRewLONG.pdf R. Banach 2020 Sci. Comp. Prog., 190, Paper 102404, 21pp., `Automated Urban Train Control with Hybrid Event-B: 'Tackling' the Rugby Club Problem.' Preprint: .../CEvB.RugbyClub.FULL.ps.gz .../CEvB.RugbyClub.FULL.pdf J. Foucault, S. Lesecq, G. Dudnik, M. Correvon, R. O'Keeffe, V. Di Palma, M. Passioni, F. Quaglia, L. Ouvry, S. Buckley, J. Herveg, A. di Matteo, T. Rakotovao, O. Debicki, N. Mareau, J. Barrett, S. Rea, A. McGibney, F. Birot, H. de Chaumont, R. Banach, J. Razavi, C. O'Murchu 2019 Sensors 19, Paper 04350, `INSPEX: Optimize Range Sensors for Environment Perception as a Portable System' Open Access: .../Sensors-2019-04350.pdf R. Banach 2018 Sci. Comp. Prog., 156, 21-44, `Modelling, Formal Refinement and Partitioning Strategies for a Small Aircraft Fuel Pump System in Hybrid Event-B.' Preprint: .../CEvB.FuelPump.FULL.ps.gz .../CEvB.FuelPump.FULL.pdf R. Banach, M. Butler, S. Qin, H. Zhu 2017 Sci. Comp. Prog., 139, 1-35, `Core Hybrid Event-B II: Multiple Cooperating Hybrid Event-B Machines.' Preprint: .../ContEvB--II.ps.gz .../ContEvB--II.pdf R. Banach 2017 Int. J. Soft. Tools for Tech. Trans., 19, 205-228, `The Landing Gear System in Multi-Machine Hybrid Event-B.' Preprint: .../CEvB.LandingGear-STTT.ps.gz .../CEvB.LandingGear-STTT.pdf R. Banach 2015 J. Soft Comp. Soft. Eng., 5, 31-54, `Model Based Refinement and the Design of Retrenchments.' Preprint: .../Retrench.Designs.ps.gz .../Retrench.Designs.pdf R. Banach, M. Butler, S. Qin, N. Verma, H. Zhu 2015 Sci. Comp. Prog., 105, 92-123, `Core Hybrid Event-B I: Single Hybrid Event-B Machines.' Preprint: .../ContEvB--I.ps.gz .../ContEvB--I.pdf R. Banach, C. Jeske 2015 Math. Struc. Comp. Sci., 25, 135-202, `Retrenchment and Refinement Interworking: the Tower Theorems.' Preprint: .../Retrench.Tower.ps.gz .../Retrench.Tower.pdf R. Banach, H. Zhu, W. Su, X. Wu 2014 ACM Trans. Soft. Eng. Meth., 24(1), Art.2, 40pp., `A Continuous ASM Modelling Approach to Pacemaker Sensing.' Preprint: .../Contin.ASM.Pace.FULL.ps.gz .../Contin.ASM.Pace.FULL.pdf R. Banach, H. Zhu, W. Su, X. Wu 2014 Sci. Comp. Prog., 94, 109-129, `ASM, Controller Synthesis, and Complete Refinement.' Preprint: .../Contin.ASM.Con.FULL.ps.gz .../Contin.ASM.Con.FULL.pdf R. Banach, H. Zhu, W. Su, R. Huang 2014 Form. Asp. Comp., 26, 319-366, `Continuous KAOS, ASM, and Formal Control System Design Across the Continuous/Discrete Modeling Interface: A Simple Train Stopping Application.' Preprint: .../Form.Cont.Sim.Train.ps.gz .../Form.Cont.Sim.Train.pdf R. Banach, M. Bozzano 2013 Form. Asp. Comp., 25, 573-607, `The Mechanical Generation of Fault Trees for Reactive Systems via Retrenchment I: Combinational Circuits.' Preprint: .../Retrench.FT.ReaSys.I.Comb.ps.gz .../Retrench.FT.ReaSys.I.Comb.pdf R. Banach, M. Bozzano 2013 Form. Asp. Comp., 25, 609-657, `The Mechanical Generation of Fault Trees for Reactive Systems via Retrenchment II: Clocked and Feedback Circuits.' Preprint: .../Retrench.FT.ReaSys.II.TimCy.ps.gz .../Retrench.FT.ReaSys.II.TimCy.pdf R. Banach, C. Jeske, A. Hall, S. Stepney 2013 Form. Asp. Comp., 25, 439-464, `Atomicity Failure and the Retrenchment Atomicity Pattern.' Preprint: .../Retrench.At.Fail.At.Patt.ps.gz .../Retrench.At.Fail.At.Patt.pdf R. Banach, C. Jeske 2011 J. Log. Alg. Prog., 80, 453-480, `Simple Feature Engineering via Neat Default Retrenchments.' Preprint: .../Retrench.Feature.ps.gz .../Retrench.Feature.pdf R. Banach 2011 Form. Asp. Comp., 23, 113-131, `Retrenchment for Event-B: UseCase-wise Development and Rodin Integration.' Preprint: .../Retrench.EventB.UC.ps.gz .../Retrench.EventB.UC.pdf R. Banach, C. Jeske 2010 J. Log. Alg. Prog., 79, 215-232, `Stronger Compositions for Retrenchments.' Preprint: .../Retrench.Strong.Comp.ps.gz .../Retrench.Strong.Comp.pdf Preprint including full proofs: .../Retrench.Strong.Comp.FULL.ps.gz .../Retrench.Strong.Comp.FULL.pdf R. Banach, G. Schellhorn 2010 Form. Asp. Comp., 22, 33-61, `Atomic Actions and their Refinements to Isolated Protocols.' Preprint: .../Refine.At.Act.Prot.ps.gz .../Refine.At.Act.Prot.pdf R. Banach, C. Jeske, M. Poppleton 2008 J. Log. Alg. Prog., 75, 209-229, `Composition Mechanisms for Retrenchment.' Preprint: .../Retrench.Composition.ps.gz .../Retrench.Composition.pdf R. Banach, M. Poppleton, C. Jeske, S. Stepney 2007 Sci. Comp. Prog., 67, 301-329, `Engineering and Theoretical Underpinnings of Retrenchment.' Preprint: .../Retrench.Underpin.ps.gz .../Retrench.Underpin.pdf R. Banach, C. Jeske, M. Poppleton, S. Stepney 2007 Fund. Inf., 77, 29-69, `Retrenching the Purse: The Balance Enquiry Quandary, and Generalised and (1,1) Forward Refinements.' Preprint: .../Retrench.Mondex.Bal.ps.gz .../Retrench.Mondex.Bal.pdf R. Banach, J-P. Bodeveix, M. Filali, M. Poppleton 2005 Ann. Math., Comp. and Teleinf., 1, 18-26, `Dynamic Aspects of Retrenchments through Temporal Logic.' Preprint: .../Retrench.Dyn.Asp.TL.ACMT.ps.gz .../Retrench.Dyn.Asp.TL.ACMT.pdf R. Banach, M. Poppleton 2003 Req. Eng. J., 8, 266-288, `Retrenching Partial Requirements into System Definitions: A Simple Feature Interaction Case Study.' Preprint: .../Retrench.Partial.Req.ps.gz .../Retrench.Partial.Req.pdf R. Banach, F. Arbab, G.A. Papadopoulos, J.R.W. Glauert 2003 J. Univ. Comp. Sci., 9, 2-33, `A Multiply Hierarchical Automaton Semantics for the IWIM Coordination Model.' http://www.iicm.edu/jucs Preprint: .../IWIM.Medium.ps.gz .../IWIM.Medium.pdf R. Banach, M. Poppleton 1999 Form. Asp. Comp., 11, 498-540, `Sharp Retrenchment, Modulated Refinement, and Simulation.' Preprint: .../Sharp.Retrench.ps.gz .../Sharp.Retrench.pdf R. Banach 1997 J. Univ. Comp. Sci., 3, 1283-1336, `MONSTR V --- Transitive Coercing Semantics and the Church-Rosser Property.' http://www.iicm.edu/jucs Preprint: .../MONSTR-V.ps.gz .../MONSTR-V.pdf R. Banach, G.A. Papadopoulos 1997 J. Prog. Lang., 5, 201-231, `A Study of Two Graph Rewriting Formalisms: Interaction Nets and MONSTR.' http://www.chapmanhall.com/jp/ Preprint: .../Study.IN.MONSTR.ps.gz .../Study.IN.MONSTR.pdf R. Banach 1997 J. Univ. Comp. Sci., 3, 755-801, `MONSTR II --- Suspending Semantics and Independence.' http://www.iicm.edu/jucs Preprint: .../MONSTR-II.ps.gz .../MONSTR-II.pdf R. Banach 1996 Inf. Proc. Lett., 60, 109-114, `Transitive Term Graph Rewriting.' Preprint: .../Trans.TGR.ps.gz .../Trans.TGR.pdf R. Banach 1996 J. Univ. Comp. Sci., 2, 164-216, `MONSTR I --- Fundamental Issues and the Design of MONSTR.' http://www.iicm.edu/jucs Preprint: .../MONSTR-I.ps.gz .../MONSTR-I.pdf (Corrigendum: Vol. 2 No. 12) .../MONSTR-I.corr.ps.gz .../MONSTR-I.corr.pdf R. Banach 1995 Sci. Comp. Prog., 24, 221-248, `On Regularity in Software Design.' Preprint: .../Regularity.Sw.Des.ps.gz .../Regularity.Sw.Des.pdf R. Banach 1995 Theor. Comp. Sci., 152, 305-320, `Locating the Contractum in the Double Pushout Approach.' R. Banach, J. Balazs, G.A. Papadopoulos 1995 J. Univ. Comp. Sci., 1, 335-394, `A Translation of the Pi-Calculus into MONSTR.' http://www.iicm.edu/jucs Preprint: .../Pi.MONSTR.ps.gz .../Pi.MONSTR.pdf R. Banach 1995 Ann. Pure App. Logic, 73, 277-295, `Sequent Reconstruction in LLM: A Sweepline Proof.' R. Banach 1994 Theor. Comp. Sci., 131, 29-94, Fundamental Study, `Term Graph Rewriting and Garbage Collection Using Opfibrations.' R. Banach 1994 Theor. Comp. Sci., 129, 187-192, `Regular Relations and Bicartesian Squares.' R. Banach 1993 J. Pure App. Alg., 86, 7-22, `Weak Fibrations.'