JACK: A Framework for Process Algebra Implementation in Java. - Leonardo Freitas; Augusto Sampaio 001; Ana Cavalcanti 001 (SBES, 2002)

Operational Semantics for Model Checking Circus. - Jim Woodcock 001; Ana Cavalcanti 001; Leonardo Freitas (FM, 2005)

CZT Support for Z Extensions. - Tim Miller 001; Leo Freitas; Petra Malik; Mark Utting (IFM, 2005)

Model checking Circus. - Leonardo Freitas (2005)

Taking Our Own Medicine: Applying the Refinement Calculus to State-Rich Refinement Model Checking. - Leo Freitas; Ana Cavalcanti 001; Jim Woodcock 001 (ICFEM, 2006)

Z/Eves and the Mondex Electronic Purse. - Jim Woodcock 001; Leo Freitas (ICTAC, 2006)

State-rich model checking. - Leo Freitas; Jim Woodcock 001; Ana Cavalcanti 001 (Innov. Syst. Softw. Eng., 2006)

Proving Theorems About JML Classes. - Leo Freitas; Jim Woodcock 001 (Formal Methods and Hybrid Real-Time Systems, 2007)

Verifying the CICS File Control API with Z/Eves: An Experiment in the Verified Software Repository. - Leo Freitas; Konstantinos Mokos; Jim Woodcock 001 (ICECCS, 2007)

A formal security policy for xenon. - John P. McDermott; Leo Freitas (FMSE, 2008)

POSIX and the Verification Grand Challenge: A Roadmap. - Leo Freitas; Jim Woodcock 001; Andrew Butterfield (ICECCS, 2008)

Linking VDM and Z. - Jim Woodcock 001; Leo Freitas (ICECCS, 2008)

UTP and Temporal Logic Model Checking. - Hugh Anderson; Gabriel Ciobanu; Leo Freitas (UTP, 2008)

Mechanising Mondex with Z/Eves. - Leo Freitas; Jim Woodcock 001 (Formal Aspects Comput., 2008)

Mechanising Data-Types for Kernel Design in Z. - Leo Freitas (SBMF, 2009)

FDR Explorer. - Leo Freitas; Jim Woodcock 001 (Formal Aspects Comput., 2009)

A Chain Datatype in Z. - Leo Freitas; Jim Woodcock 001 (Int. J. Softw. Informatics, 2009)

Mechanising a formal model of flash memory. - Andrew Butterfield; Leo Freitas; Jim Woodcock 001 (Sci. Comput. Program., 2009)

POSIX file store in Z/Eves: An experiment in the verified software repository. - Leo Freitas; Jim Woodcock 001; Zheng Fu (Sci. Comput. Program., 2009)

Verifying the CICS File Control API with Z/Eves: An experiment in the verified software repository. - Leo Freitas; Jim Woodcock 001; Yichi Zhang (Sci. Comput. Program., 2009)

Using formal methods for security in the Xenon project. - John P. McDermott; Leo Freitas (CSIIRW, 2010)

Formal Modelling of Separation Kernel Components. - Andrius Velykis; Leo Freitas (ICTAC, 2010)

Formal methods for security in the Xenon hypervisor. - Leo Freitas; John P. McDermott (Int. J. Softw. Tools Technol. Transf., 2011)

Formalising Workflows Partitioning over Federated Clouds: Multi-level Security and Costs. - Leo Freitas; Paul Watson 001 (SERVICES, 2012)

Ours Is to Reason Why. - Cliff B. Jones; Leo Freitas; Andrius Velykis (Theories of Programming and Formal Methods, 2013)

Can a system learn from interactive proofs? - Leo Freitas; Cliff B. Jones; Andrius Velykis (HOWARD-60, 2014)

Harvesting High Value Foreign Currency Transactions from EMV Contactless Credit Cards Without the PIN. - Martin Emms; Budi Arief; Leo Freitas; Joseph Hannon; Aad P. A. van Moorsel (CCS, 2014)

Proof Patterns for Formal Methods. - Leo Freitas; Iain Whiteside (FM, 2014)

A Model for Capturing and Replaying Proof Strategies. - Leo Freitas; Cliff B. Jones; Andrius Velykis; Iain Whiteside (VSTTE, 2014)

Formalizing workflows partitioning over federated clouds: multi-level security and costs. - Leo Freitas; Paul Watson 001 (Int. J. Comput. Math., 2014)

Safety-Critical Java Virtual Machine Services. - James Baxter 001; Ana Cavalcanti 001; Andy J. Wellings; Leo Freitas (JTRES, 2015)

Modelling and Verifying a Priority Scheduler for an SCJ Runtime Environment. - Leo Freitas; James Baxter 001; Ana Cavalcanti 001; Andy J. Wellings (IFM, 2016)

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

Safety Analysis of Software Components of a Dialysis Machine Using Model Checking. - Michael D. Harrison; Michael J. Drinnan; José Creissac Campos; Paolo Masci 001; Leo Freitas; Costanzo di Maria; Michael Whitaker (FACS, 2017)

VDM at Large: Modelling the EMV® 2^nd 2 nd Generation Kernel. - Leo Freitas (SBMF, 2018)

A Methodology for Protocol Verification Applied to EMV® 1. - Leo Freitas; Paolo Modesti; Martin Emms (SBMF, 2018)

Formal techniques in the safety analysis of software components of a new dialysis machine. - Michael D. Harrison; Leo Freitas; Michael J. Drinnan; José Creissac Campos; Paolo Masci 001; Costanzo di Maria; Michael Whitaker (Sci. Comput. Program., 2019)

Account and Transaction Protocol of the Open Banking Standard. - Abdulaziz Almehrej; Leo Freitas; Paolo Modesti (ABZ, 2020)

Security Analysis of the Open Banking Account and Transaction API Protocol. - Abdulaziz Almehrej; Leo Freitas; Paolo Modesti (CoRR, 2020)

Medicine-by-wire: Practical considerations on formal techniques for dependable medical systems. - Leo Freitas; William E. Scott III; Patrick Degenaar (Sci. Comput. Program., 2020)

Digital Twins for Organ Preservation Devices. - Aaron John Buhagiar; Leo Freitas; William E. Scott III; Peter Gorm Larsen (ISoLA (4), 2022)

Specification-based CSV Support in VDM. - Leo Freitas; Aaron John Buhagiar (CoRR, 2023)

VDM recursive functions in Isabelle/HOL. - Leo Freitas; Peter Gorm Larsen (CoRR, 2023)

Topologically sorting VDM-SL definitions for Isabelle/HOL translation. - Leo Freitas (CoRR, 2023)

International System of Quantities library in VDM. - Leo Freitas (CoRR, 2023)

Proceedings of the 22nd International Overture Workshop. - Hugo Daniel Macedo; Ken Pierce; Leo Freitas (CoRR, 2024)

Verification Technology for VDM: Craft and Automation. - John S. Fitzgerald; Peter Gorm Larsen; Ken Pierce; Leo Freitas; Nick Battle (The Practice of Formal Methods (I), 2024)

SmartAudits: Applying Timebands to a Medical Device. - Leo Freitas; Aaron John Buhagiar; William E. Scott III (The Practice of Formal Methods (I), 2024)

Translating a VDM Model of a Medical Device into Kapture. - Joe Hare; Leo Freitas; Ken Pierce (CoRR, 2025)