Expression Transformers in B-GSL. - Bill Stoddart; Frank Zeyda (ZB, 2003)

A Prospective-Value Semantics for the GSL. - Frank Zeyda; Bill Stoddart; Steve Dunne (ZB, 2005)

A Design-Based Model of Reversible Computation. - Bill Stoddart; Frank Zeyda; Robert Lynas (UTP, 2006)

Modelling and Proof Analysis of Interrupt Driven Scheduling. - Bill Stoddart; Dominique Cansell; Frank Zeyda (B, 2007)

Reversible computations in B. - Frank Zeyda (2007)

Encoding Circus Programs in ProofPowerZ. - Frank Zeyda; Ana Cavalcanti 001 (UTP, 2008)

Mechanised Translation of Control Law Diagrams into Circus. - Frank Zeyda; Ana Cavalcanti 001 (IFM, 2009)

A Virtual Machine for Supporting Reversible Probabilistic Guarded Command Languages. - Bill Stoddart; Robert Lynas; Frank Zeyda (RC@ETAPS, 2009)

Supporting ArcAngel in ProofPower. - Frank Zeyda; Marcel Oliveira; Ana Cavalcanti 001 (REFINE@FMWeek, 2009)

Reactivising Classical B. - Steve Dunne; Frank Zeyda (ASM, 2010)

Communication Systems in ClawZ. - Michael Vernon; Frank Zeyda; Ana Cavalcanti 001 (ASM, 2010)

Preference and Non-deterministic Choice. - Bill Stoddart; Frank Zeyda; Steve Dunne (ICTAC, 2010)

Automating Refinement of Circus Programs. - Frank Zeyda; Ana Cavalcanti 001 (SBMF, 2010)

The Safety-Critical Java Mission Model: A Formal Account. - Frank Zeyda; Ana Cavalcanti 001; Andy J. Wellings (ICFEM, 2011)

Safety-critical Java in Circus. - Ana Cavalcanti 001; Andy J. Wellings; Jim Woodcock 001; Kun Wei; Frank Zeyda (JTRES, 2011)

A tactic language for refinement of state-rich concurrent specifications. - Marcel Oliveira; Frank Zeyda; Ana Cavalcanti 001 (Sci. Comput. Program., 2011)

A Tool Chain for the Automatic Generation of Circus Specifications of Simulink Diagrams. - Chris Marriott; Frank Zeyda; Ana Cavalcanti 001 (ABZ, 2012)

Higher-Order UTP for a Theory of Methods. - Frank Zeyda; Ana Cavalcanti 001 (UTP, 2012)

Mechanised support for sound refinement tactics. - Frank Zeyda; Marcel Oliveira; Ana Cavalcanti 001 (Formal Aspects Comput., 2012)

Mechanical reasoning about families of UTP theories. - Frank Zeyda; Ana Cavalcanti 001 (Sci. Comput. Program., 2012)

Refining SCJ Mission Specifications into Parallel Handler Designs - Frank Zeyda; Ana Cavalcanti 001 (Refine@IFM, 2013)

A unification of probabilistic choice within a design-based model of reversible computation. - Bill Stoddart; Frank Zeyda (Formal Aspects Comput., 2013)

Safety-critical Java programs from Circus models. - Ana Cavalcanti 001; Frank Zeyda; Andy J. Wellings; Jim Woodcock 001; Kun Wei (Real Time Syst., 2013)

A Modular Theory of Object Orientation in Higher-Order UTP. - Frank Zeyda; Thiago L. V. L. Santos; Ana Cavalcanti 001; Augusto Sampaio 001 (FM, 2014)

Isabelle/UTP: A Mechanised Theory Engineering Framework. - Simon Foster 001; Frank Zeyda; Jim Woodcock 001 (UTP, 2014)

Circus Models for Safety-Critical Java Programs. - Frank Zeyda; Lalkhumsanga Lalkhumsanga; Ana Cavalcanti 001; Andy J. Wellings (Comput. J., 2014)

An Empirical Analysis of Neurofeedback Using PID Control Systems. - Frank Zeyda; Gabor Aranyi; Fred Charles; Marc Cavazza (SMC, 2015)

Laws of mission-based programming. - Frank Zeyda; Ana Cavalcanti 001 (Formal Aspects Comput., 2015)

Unifying Heterogeneous State-Spaces with Lenses. - Simon Foster 001; Frank Zeyda; Jim Woodcock 001 (ICTAC, 2016)

An Axiomatic Value Model for Isabelle/UTP. - Frank Zeyda; Simon Foster 001; Leo Freitas (UTP, 2016)

Formalising Cosimulation Models. - Frank Zeyda; Julien Ouy; Simon Foster 001; Ana Cavalcanti 001 (SEFM Workshops, 2017)

Optics. - Simon Foster 001; Frank Zeyda (Arch. Formal Proofs, 2017)

Unifying Theories of Timed with Generalised Reactive Processes. - Simon Foster 001; Ana Cavalcanti 001; Jim Woodcock 001; Frank Zeyda (CoRR, 2017)

Modeling and analysis of the disruptor framework in CSP. - Yucheng Fang; Huibiao Zhu; Frank Zeyda; Yuan Fei (CCWC, 2018)

Unifying theories of time with generalised reactive processes. - Simon Foster 001; Ana Cavalcanti 001; Jim Woodcock 001; Frank Zeyda (Inf. Process. Lett., 2018)

Isabelle/UTP: Mechanised Theory Engineering for Unifying Theories of Programming. - Simon Foster 001; Frank Zeyda; Yakoub Nemouchi; Pedro Ribeiro 002; Burkhart Wolff (Arch. Formal Proofs, 2019)

Bunch theory, applications, axioms and models. - Bill Stoddart; Frank Zeyda; Steve Dunne (CoRR, 2019)

Unifying semantic foundations for automated verification tools in Isabelle/UTP. - Simon Foster 001; James Baxter 001; Ana Cavalcanti 001; Jim Woodcock 001; Frank Zeyda (Sci. Comput. Program., 2020)

Unifying theories of reactive design contracts. - Simon Foster 001; Ana Cavalcanti 001; Samuel Canham; Jim Woodcock 001; Frank Zeyda (Theor. Comput. Sci., 2020)

UTP, Circus, and Isabelle. - Jim Woodcock 001; Ana Cavalcanti 001; Simon Foster 001; Marcel Oliveira; Augusto Sampaio 001; Frank Zeyda (Theories of Programming and Formal Methods, 2023)

bGSL: An imperative language for specification and refinement of backtracking programs. - Steve Dunne; João F. Ferreira 001; Alexandra Mendes; Campbell Ritchie; Bill Stoddart; Frank Zeyda (J. Log. Algebraic Methods Program., 2023)

A Tour Through the Programming Choices: Semantics and Applications. - Pedro Ribeiro 002; Kangfeng Ye; Frank Zeyda; Alvaro Miyazawa (The Application of Formal Methods, 2024)

Bunch theory: Axioms, logic, applications and model. - Bill Stoddart; Steve Dunne; Chunyan Mu; Frank Zeyda (J. Log. Algebraic Methods Program., 2024)