Frank Zeyda

Search results

• 2024

  A Tour Through the Programming Choices: Semantics and Applications

  Ribeiro, P., Ye, K., Zeyda, F. & Miyazawa, A., 1 Sept 2024, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics): The Application of Formal Methods. Foster, S. & Sampaio, A. (eds.). Springer Science and Business Media Deutschland GmbH, Vol. 14900. p. 261-305 45 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 14900 LNCS).

  Research output: Chapter in Book/Report/Conference proceeding › Chapter

  Open Access

  File
• 2023

  UTP, Circus, and Isabelle

  Woodcock, J., Cavalcanti, A., Foster, S., Oliveira, M., Sampaio, A. & Zeyda, F., 8 Sept 2023, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). Springer Science and Business Media Deutschland GmbH, p. 19-51 33 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 14080 LNCS).

  Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

  Open Access

  File
• 2020

  Unifying Semantic Foundations for Automated Verification Tools in Isabelle/UTP

  Foster, S. D., Baxter, J., Cavalcanti, A. L. C., Woodcock, J. & Zeyda, F., 26 Jun 2020, (E-pub ahead of print) In: Science of Computer Programming. 197, 40 p., 102510.

  Research output: Contribution to journal › Article › peer-review

  Open Access

  File

• Unifying Theories of Reactive Design Contracts

  Foster, S. D., Cavalcanti, A. L. C., Canham, S. J., Woodcock, J. C. P. & Zeyda, F., 8 Jan 2020, In: Theoretical Computer Science. 802, p. 105-140

  Research output: Contribution to journal › Article › peer-review

  Open Access

  File
• 2019

  Isabelle/UTP: Mechanised Theory Engineering for Unifying Theories of Programming

  Foster, S. D., Zeyda, F., Nemouchi, Y., De Oliveira Salazar Ribeiro, P. F. & Wolff, B., 11 Jun 2019, In: Archive of Formal Proofs. 168 p.

  Research output: Contribution to journal › Article › peer-review

  Open Access

  File
• 2018

  Isabelle/UTP: Mechanised Theory Engineering for the UTP

  Foster, S. D., Zeyda, F., Nemouchi, Y., De Oliveira Salazar Ribeiro, P. F. & Wolff, B., 4 Apr 2018, (Unpublished) 162 p.

  Research output: Working paper

  File

• Theory of Designs in Isabelle/UTP

  Foster, S. D., Nemouchi, Y. & Zeyda, F., 6 Apr 2018, (Unpublished) 47 p.

  Research output: Working paper

  File

• Unifying Theories of Time with Generalised Reactive Processes

  Foster, S. D., Cavalcanti, A. L. C., Woodcock, J. C. P. & Zeyda, F., Jul 2018, In: Information Processing Letters. 135, p. 47-52 6 p.

  Research output: Contribution to journal › Article › peer-review

  Open Access

  File
• 2017

  Formalising Cosimulation Models

  Zeyda, F., Ouy, J., Foster, S. D. & Cavalcanti, A. L. C., Sept 2017, (E-pub ahead of print) 1st Workshop on Formal Co-Simulation of Cyber-Physical Systems (CoSim-CPS 2017). 15 p.

  Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

  Open Access

  File

• Optics in Isabelle/HOL

  Foster, S. D. & Zeyda, F., 1 Jun 2017, In: Archive of Formal Proofs. p. 1-28 28 p.

  Research output: Contribution to journal › Article › peer-review

  Open Access

  File
• 2016

  Unifying heterogeneous state-spaces with lenses

  Foster, S., Zeyda, F. & Woodcock, J., 24 Oct 2016, Theoretical Aspects of Computing - ICTAC 2016, 13th International Colloquium, Proceedings. Wang, F. & Sampaio, A. (eds.). Springer, p. 295-314 20 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 9965 LNCS).

  Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

  Open Access

  File
• 2015

  Isabelle/UTP: A Mechanised Theory Engineering Framework

  Foster, S., Zeyda, F. & Woodcock, J., 6 Jan 2015, Unifying Theories of Programming : 5th International Symposium, UTP 2014, Singapore, May 13, 2014, Revised Selected Papers. Naumann, D. (ed.). Springer, Vol. 8963. p. 21-41 21 p. (Lecture Notes in Computer Science).

  Research output: Chapter in Book/Report/Conference proceeding › Chapter (peer-reviewed) › peer-review

  Open Access

  File

• Laws of mission-based programming

  Cavalcanti, A. L. C. & Zeyda, F., Jan 2015, In: Formal Aspects of Computing. 27, p. 423-472 50 p.

  Research output: Contribution to journal › Article › peer-review
• 2014

  A modular theory of object orientation in higher-order UTP

  Zeyda, F., Santos, T. L. V. L., Cavalcanti, A. L. C. & Sampaio, A. C. A., 2014, FM 2014: Formal Methods: 19th International Symposium, Singapore, May 12-16, 2014. Proceedings. Springer, p. 627-642 16 p. (Lecture Notes in Computer Science; vol. 8442).

  Research output: Chapter in Book/Report/Conference proceeding › Conference contribution
• 2013

  Circus Models for Safety-Critical Java Programs

  Zeyda, F., Lalkhumsanga, L., Cavalcanti, A. L. C. & Wellings, A. J., 2013, In: The Computer Journal. 57, 7, p. 1046-1091 46 p.

  Research output: Contribution to journal › Article › peer-review

• Higher-Order UTP in Theories of Object-Orientation

  Zeyda, F. & Cavalcanti, A. L. C., 2013, 4th International Symposium on Unifying Theories of Programming. Springer, Vol. 7681. p. 204-223 (Lecture Notes in Computer Science; vol. 7681).

  Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

• Refining SCJ Mission Specifications into Parallel Handler Designs

  Zeyda, F. & Cavalcanti, A., 27 May 2013, In: Electronic Proceedings in Theoretical Computer Science. 115, p. 52-67 16 p.

  Research output: Contribution to journal › Article › peer-review

• Safety-critical Java programs from Circus models

  Cavalcanti, A. L. C., Zeyda, F., Wellings, A., Woodcock, J. & Wei, K., Sept 2013, In: Real-Time Systems. 49, 5, p. 614-667 54 p.

  Research output: Contribution to journal › Article › peer-review
• 2012

  A Tool Chain for the Automatic Generation of Circus Specifications of Simulink Diagrams.

  Marriott, C., Zeyda, F. & Cavalcanti, A. L. C., 2012, Abstract State Machines, Alloy, B, VDM, and Z. Vol. 7316. p. 294-307

  Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

• Mechanical reasoning about families of UTP theories

  Zeyda, F. & Cavalcanti, A. L. C., 1 Apr 2012, In: Science of Computer Programming. 77, 4, p. 444-479 36 p.

  Research output: Contribution to journal › Article › peer-review

• Mechanised support for sound refinement tactics

  Zeyda, F., Oliveira, M. & Cavalcanti, A. L. C., 1 Jan 2012, In: Formal Aspects of Computing. 24, 1, p. 127-160 34 p.

  Research output: Contribution to journal › Article › peer-review
• 2011

  A tactic language for refinement of state-rich concurrent specifications

  Oliveira, M., Zeyda, F. & Cavalcanti, A., 1 Sept 2011, In: Science of Computer Programming. 76, 9, p. 792-833 42 p.

  Research output: Contribution to journal › Article › peer-review

• Safety-Critical Java in Circus

  Cavalcanti, A. L. C., Wellings, A., Woodcock, J., Wei, K. & Zeyda, F., 2011, 9th Workshop on Java Technologies for Real-Time and Embedded System. p. 20-29 10 p.

  Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

• The Safety-critical Java Mission Model: a formal account

  Zeyda, F., Cavalcanti, A. L. C. & Wellings, A., 2011, International Conference on Formal Engineering Methods. Vol. 6991 LNCS. p. 49-65 17 p.

  Research output: Chapter in Book/Report/Conference proceeding › Conference contribution
• 2010

  Automating Refinement of Circus Programs

  Zeyda, F. & Cavalcanti, A., 2010, p. 274-290.

  Research output: Contribution to conference › Paper › peer-review

• Communication Systems in ClawZ

  Vernon, M., Zeyda, F. & Cavalcanti, A., 2010, p. 334-348.

  Research output: Contribution to conference › Paper › peer-review

• Encoding Circus programs in ProofPower-Z

  Zeyda, F. & Cavalcanti, A., 26 Aug 2010, Unifying Theories of Programming - Second International Symposium, UTP 2008, Revised Selected Papers. p. 218-237 20 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 5713 LNCS).

  Research output: Chapter in Book/Report/Conference proceeding › Conference contribution
• 2009

  Mechanical Reasoning about Families of UTP Theories

  Zeyda, F. & Cavalcanti, A., 2 Jul 2009, In: Electronic Notes in Theoretical Computer Science. 240, C, p. 239-257 19 p.

  Research output: Contribution to journal › Article › peer-review

• Mechanised Translation of Control Law Diagrams into Circus

  Zeyda, F. & Cavalcanti, A., 2009, p. 151-166.

  Research output: Contribution to conference › Paper › peer-review

• Mechanised Translation of Control Law Diagrams into Circus

  Zeyda, F. & Cavalcanti, A., 2009, Integrated Formal Methods. Leuschel, M. & Wehrheim, H. (eds.). Springer, Vol. 5423 LNCS. p. 151-166 16 p. (Lecture Notes in Computer Science; vol. 2999).

  Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

• Supporting ArcAngel in ProofPower

  Zeyda, F., Oliveira, M. & Cavalcanti, A., 31 Dec 2009, In: Electronic Notes in Theoretical Computer Science. 259, C, p. 225-243 19 p.

  Research output: Contribution to journal › Article › peer-review
• 2008

  Encoding it ircus Programs in ProofPowerZ

  Zeyda, F. & Cavalcanti, A., 2008, p. 218-237.

  Research output: Contribution to conference › Paper › peer-review