Frank Zeyda

Orcid: 0009-0009-4251-4740

According to our database1, Frank Zeyda authored at least 41 papers between 2003 and 2023.

Collaborative distances:



In proceedings 
PhD thesis 


Online presence:



bGSL: An imperative language for specification and refinement of backtracking programs.
J. Log. Algebraic Methods Program., 2023

UTP, Circus, and Isabelle.
Proceedings of the Theories of Programming and Formal Methods, 2023

Unifying theories of reactive design contracts.
Theor. Comput. Sci., 2020

Unifying semantic foundations for automated verification tools in Isabelle/UTP.
Sci. Comput. Program., 2020

Bunch theory, applications, axioms and models.
CoRR, 2019

Isabelle/UTP: Mechanised Theory Engineering for Unifying Theories of Programming.
Arch. Formal Proofs, 2019

Unifying theories of time with generalised reactive processes.
Inf. Process. Lett., 2018

Modeling and analysis of the disruptor framework in CSP.
Proceedings of the IEEE 8th Annual Computing and Communication Workshop and Conference, 2018

Unifying Theories of Timed with Generalised Reactive Processes.
CoRR, 2017

Arch. Formal Proofs, 2017

Formalising Cosimulation Models.
Proceedings of the Software Engineering and Formal Methods, 2017

An Axiomatic Value Model for Isabelle/UTP.
Proceedings of the Unifying Theories of Programming - 6th International Symposium, 2016

Unifying Heterogeneous State-Spaces with Lenses.
Proceedings of the Theoretical Aspects of Computing - ICTAC 2016, 2016

Laws of mission-based programming.
Formal Aspects Comput., 2015

An Empirical Analysis of Neurofeedback Using PID Control Systems.
Proceedings of the 2015 IEEE International Conference on Systems, 2015

<i>Circus</i> Models for Safety-Critical Java Programs.
Comput. J., 2014

Isabelle/UTP: A Mechanised Theory Engineering Framework.
Proceedings of the Unifying Theories of Programming - 5th International Symposium, 2014

A Modular Theory of Object Orientation in Higher-Order UTP.
Proceedings of the FM 2014: Formal Methods, 2014

Safety-critical Java programs from Circus models.
Real Time Syst., 2013

A unification of probabilistic choice within a design-based model of reversible computation.
Formal Aspects Comput., 2013

Refining SCJ Mission Specifications into Parallel Handler Designs
Proceedings of the Proceedings 16th International Refinement Workshop, 2013

Mechanised support for sound refinement tactics.
Formal Aspects Comput., 2012

Higher-Order UTP for a Theory of Methods.
Proceedings of the Unifying Theories of Programming, 4th International Symposium, 2012

A Tool Chain for the Automatic Generation of Circus Specifications of Simulink Diagrams.
Proceedings of the Abstract State Machines, Alloy, B, VDM, and Z, 2012

A tactic language for refinement of state-rich concurrent specifications.
Sci. Comput. Program., 2011

Safety-critical Java in Circus.
Proceedings of the 9th International Workshop on Java Technologies for Real-time and Embedded Systems, 2011

The Safety-Critical Java Mission Model: A Formal Account.
Proceedings of the Formal Methods and Software Engineering, 2011

Automating Refinement of <i>Circus</i> Programs.
Proceedings of the Formal Methods: Foundations and Applications, 2010

Preference and Non-deterministic Choice.
Proceedings of the Theoretical Aspects of Computing, 2010

Communication Systems in ClawZ.
Proceedings of the Abstract State Machines, 2010

Reactivising Classical B.
Proceedings of the Abstract State Machines, 2010

Supporting ArcAngel in ProofPower.
Proceedings of the 14th BCS-FACS Refinement Workshop, 2009

A Virtual Machine for Supporting Reversible Probabilistic Guarded Command Languages.
Proceedings of the Workshop on Reversible Computation, 2009

Mechanised Translation of Control Law Diagrams into Circus.
Proceedings of the Integrated Formal Methods, 7th International Conference, 2009

Mechanical Reasoning about Families of UTP Theories.
Proceedings of the Eleventh Brazilian Symposium on Formal Methods, 2008

Encoding <i>Circus</i> Programs in ProofPowerZ.
Proceedings of the Unifying Theories of Programming, Second International Symposium, 2008

Reversible computations in B.
PhD thesis, 2007

Modelling and Proof Analysis of Interrupt Driven Scheduling.
Proceedings of the B 2007: Formal Specification and Development in B, 2007

A Design-Based Model of Reversible Computation.
Proceedings of the Unifying Theories of Programming, First International Symposium, 2006

A Prospective-Value Semantics for the GSL.
Proceedings of the ZB 2005: Formal Specification and Development in Z and B, 2005

Expression Transformers in B-GSL.
Proceedings of the ZB 2003: Formal Specification and Development in Z and B, 2003