NuCore members

Introduction

I am interested in formal specification and verification of safety critical systems. In particular, the use of theorem provers and modelling tools. Earlier in my career I participated in the Grand Challenge in Software Verification working on: the Mondex Purse verification; verified NAND flash hardware and software; the Tokeneer ID station verification; etc. 

Since 2014, I've been involved in the dependability and design of safety critical medical devices. I worked with a novel neonatal heamodialyser through to certification, a brain pacemaker for epilepsy (and other brain ailments) control, and more recently a organ transplant preservation machine, which has become a University spin out (https://www.scubatx.com).

Since 2017, I started collaboration with EMVCo on the analysis of their new EMV2 payment protocol suite. I also worked with MasterCard on the verification/validation of their current NFC protocol. This has led to research interest and project in collaboration with the UK NCSC as a PhD studentship for the Payment Calculus project.

Research Interests

Formal specification and verification of systems through theorem proving and model checking.

• Almehrej A, Freitas L, Modesti P. Account and Transaction Protocol of the Open Banking Standard. In: International Conference on Rigorous State-Based Methods. 2020, Ulm, Germany: Springer.
• Freitas L, Emms M. Analysis of EMV 2nd Generation Kernel Specific Golden Paths. EMVCo, 2020.
• Kennedy S, Freitas L, Hardy A, Downsland S, Turner M. Clinical Prioritisation Assistance Tool (CPAT) for COVID-19. [program]. 2020.
• Emms M, Freitas L. Mastercard Contactless Reader specification verification. MasterCard, 2020.
• Freitas L, Scott III WE, Degenaar P. Medicine-by-wire: Practical considerations on formal techniques for dependable medical systems. Science of Computer Programming 2020, 200, 102545.
• Harrison MD, Freitas L, Drinnan M, Campos JC, Masci P, Di Maria C, Whitaker M. Formal Techniques in the Safety Analysis of Software Components of a new Dialysis Machine. Science of Computer Programming 2019, 175, 17-34.
• Freitas L, Modesti P, Emms M. A methodology for protocol verification applied to EMV^® 1. In: 21st Brazilian Symposium on Formal Methods (SBMF 2018). 2018, Salvador, Brazil: Springer Verlag.
• Freitas L, Emms M. Analysing the EMV 2nd generation kernel. EMVCo, 2018.
• Freitas L. VDM at Large: Modelling the EMV^® 2^nd Generation Kernel. In: Formal Methods: Foundations and Applications. 21st Brazilian Symposium (SBMF 2018). 2018, Salvador, Brazil: Springer.
• Freitas L, Emms M. Protocol Correctness Analysis EMV 2nd Generation Specifications - Formal specification of EMV 2nd Generation Kernel. EMVCo, 2017.
• Harrison MD, Drinnan M, Campos JC, Masci P, Freitas L, di Maria C, Whitaker M. Safety Analysis of Software Components of a Dialysis Machine Using Model Checking. In: Formal Aspects of Component Software (FACS 2017). 2017, Braga, Portugal: Springer.
• Zeyda F, Foster S, Freitas L. An Axiomatic Value Model for Isabelle/UTP. In: 6th International Symposium on Unifying Theories of Programming (UTP 2016). 2016, Reykjavík, Iceland.
• Freitas L, Baxter J, Calvacanti A, Wellings A. Modelling and verifying a priority scheduler for an SCJ runtime environment. In: Integrated Formal Methods: 12th International Conference (iFM 2016). 2016, Reykjavík University: Springer.
• Baxter J, Cavancanti A, Wellings A, Freitas L. Safety-Critical Java Virtual Machine Services. In: Proceedings of the 13th International Workshop on Java Technologies for Real-time and Embedded Systems (JTRES 2015). 2015, Paris: ACM.
• Freitas L, Jones CB, Velykis A, Whiteside I. A Model for Capturing and Replaying Proof Strategies. In: VSTTE 2014: Verified Software: Theories, Tools and Experiments. 2014, Vienna, Austria: Springer, Cham.
• Dias D, Freitas L, Jones C. Abstracting Interference in Postconditions. Newcastle upon Tyne: School of Computing Science, University of Newcastle upon Tyne, 2014. School of Computing Science Technical Report Series 1415.
• Freitas L, Jones CB, Velykis A. Can a system learn from interactive proofs?. In: HOWARD-60. A Festschrift on the Occasion of Howard Barringer's 60th Birthday. 2014, EasyChair.
• Dias D, Freitas L. Designing an unbounded buffer in rely-guarantee. Newcastle upon Tyne: School of Computing Science, University of Newcastle upon Tyne, 2014. School of Computing Science Technical Report Series 1431.
• Freitas L, Watson P. Formalizing workflows partitioning over federated clouds: multi-level security and costs. International Journal of Computer Mathematics 2014, 91(5), 881-906.
• Emms M, Arief B, Freitas L, Hannon J, van Moorsel A. Harvesting high value foreign currency transactions from EMV contactless cards without the PIN. Newcastle upon Tyne: School of Computing Science, University of Newcastle upon Tyne, 2014. School of Computing Science Technical Report Series 1421.
• Emms M, Arief B, Freitas L, Hannon J, van Moorsel A. Harvesting High Value Foreign Currency Transactions from EMV Contactless Credit Cards Without the PIN. In: 21st ACM Conference on Computer and Communications Security (CCS). 2014, Scottsdale, Arizona, USA: ACM.
• Freitas F, Whiteside I. Proof Patterns for Formal Methods. Newcastle upon Tyne: School of Computing Science, University of Newcastle upon Tyne, 2014. School of Computing Science Technical Report Series 1399.
• Freitas L, Whiteside I. Proof Patterns for Formal Methods. In: FM 2014: Formal Methods: 19th International Symposium. 2014, Singapore: Springer.
• Emms M, Freitas L, van Moorsel A. Rigorous Design and Implementation of an Emulator for EMV Contactless Payments. Newcastle upon Tyne: School of Computing Science, University of Newcastle upon Tyne, 2014. School of Computing Science Technical Report Series 1426.
• Freitas L, Jones CB, Velykis A, Whiteside I. How to say why (in AI4FM). Newcastle upon Tyne: School of Computing Science, University of Newcastle upon Tyne, 2013. School of Computing Science Technical Report Series 1398.
• Jones CB, Freitas L, Velykis A. Ours is to reason why. In: Liu, Z., Woodcock, J., Zhu, H, ed. Theories of Programming and Formal Methods. Berlin; New York: Springer Verlag, 2013, pp.227-243.
• Mühlberg JT, Freitas L. Combining formal methods and testing: A case study on FreeRTOS. In: 11th International Conference on Software QA and Testing on Embedded Systems (QA&Test). 2011, Bilbao, Spain: SQS, Software Quality Systems.
• Freitas L, McDermott J. Formal methods for security in the Xenon hypervisor. International Journal on Software Tools Technology Transfer 2011, 13(5), 463-489.
• Velykis A, Freitas L. Formal Modelling of Separation Kernel Components. In: Theoretical Aspects of Computing: 7th International Colloquium. 2010, Natal, Rio Grande do Norte, Brazil: Springer.
• Freitas L, Jones CB. Learning from an expert's proof: AI4FM. In: UV10 (Usable Verification). 2010, Redmond, Washington, USA.
• McDermott J, Freitas L. Using formal methods for security in the Xenon project. In: 6th Annual Workshop on Cyber Security and Information Intelligence Research (CSIIRW). 2010, Oak Ridge, Tennessee, USA: ACM Press.
• Anderson H, Ciobanu G, Freitas L. UTP and Temporal Logic Model Checking. In: Unifying Theories of Programming: Second International Symposium (UTP). 2010, Dublin, Ireland: Springer.
• Freitas L, Woodcock J. A Chain Datatype in Z. International Journal of Software and Informatics 2009, 3(2), 357-374.
• Freitas L, Woodcock J. FDR Explorer. Formal Aspects of Computing 2009, 21(1-2), 133-154.
• Butterfield A, Freitas L, Woodcock J. Mechanising a formal model of flash memory. Science of Computer Programming 2009, 74(4), 219-237.
• Freitas L. Mechanising Data-Types for Kernel Design in Z. In: Formal Methods: Foundations and Applications: 12th Brazilian Symposium on Formal Methods (SBMF). 2009, Gramado, Brazil: Springer.
• Freitas L, Woodcock J, Fu Z. POSIX file store in Z/Eves: An experiment in the verified software repository. Science of Computer Programming 2009, 74(4), 238-257.
• Woodcock J, Saaltink M, Freitas L. Unifying Theories of Undefinedness. In: Broy, M., Sitou, W., Hoare, T, ed. Engineering Methods and Tools for Software Safety and Security. Amsterdam: IOS Press, 2009, pp.311-330.
• Freitas L, Woodcock J, Zhang Y. Verifying the CICS File Control API with Z/Eves: An experiment in the verified software repository. Science of Computer Programming 2009, 74(4), 197-218.
• McDermott J, Freitas L. A formal security policy for xenon. In: 6th ACM workshop on Formal methods in security engineering. 2008, Alexandria, Virginia, USA: ACM Press.
• Woodcock J, Freitas L. Linking VDM and Z. In: 13th IEEE International Conference on Engineering of Complex Computer Systems (ICECCS). 2008, Belfast, UK: IEEE.
• Freitas L, Woodcock J. Mechanising Mondex with Z/Eves. Formal Aspects of Computing 2008, 20(1), 117-139.
• Woodcock J, Cavalcanti A, Gaudel MC, Freitas L. Operational Semantics for Circus. York, UK: York University, 2008.
• Freitas L. POSIX and the Verification Grand Challenge: A Roadmap. In: 13th IEEE International Conference on Engineering of Complex Computer Systems (ICECCS). 2008, Belfast, UK: IEEE.
• Freitas L, Fu Z, Woodcock J. POSIX file store in Z/Eves: an experiment in the verified software repository. In: 12th IEEE International Conference on Engineering Complex Computer Systems (ICECCS). 2007, Auckland, New Zealand: IEEE.
• Freitas L, Woodcock J. Proving Theorems About JML Classes. In: Jones, C.B., Liu, Z., Woodcock, J, ed. Formal Methods and Hybrid Real-Time Systems. Berlin: Springer, 2007, pp.255-279.
• Freitas L, Mokos K, Woodcock J. Verifying the CICS File Control API with Z/Eves: An Experiment in the Verified Software Repository. In: 12th IEEE International Conference on Engineering Complex Computer Systems (ICECCS). 2007, Auckland, New Zealand: IEEE.
• Bicarregui JC, Woodcock JCP, Freitas L, Schellhorn G, Ramananandro T, Bowen J, Banach R, Butler M, Crocker D, George C, Haxthausen A, Jackson M. Mondex Case Study Second Workshop. In: Mondex Case Study Second Workshop. 2006, Abingdon, UK.
• Freitas L, Woodcock J, Cavalcanti A. State-rich model checking. Innovations in Systems and Software Engineering 2006, 2(1), 49-64.
• Freitas L, Cavalcanti A, Woodcock J. Taking Our Own Medicine: Applying the Refinement Calculus to State-Rich Refinement Model Checking. In: Formal Methods and Software Engineering: 8th International Conference on Formal Engineering Methods (ICFEM). 2006, Macao, China: Springer.
• Woodcock J, Freitas L. Z/Eves and the Mondex Electronic Purse. In: Theoretical Aspects of Computing: Third International Colloquium (ICTAC). 2006, Tunis, Tunisia: Springer.
• Miller T, Freitas L, Malik P, Utting M. CZT Support for Z Extensions. In: Integrated Formal Methods: 5th International Conference (IFM). 2005, Eindhoven, The Netherlands: Springer.
• Woodcock J, Cavalcanti A, Freitas L. Operational Semantics for Model Checking Circus. In: Formal Methods: International Symposium of Formal Methods (FM). 2005, Newcastle upon Tyne, UK: Springer.
• Freitas L, Cavalcanti ALC, Sampaio A. JACK: A Framework for Process Algebra Implementation in Java. In: XVI Simpósio Brasileiro de Engenharia de Software. 2002, Gramado, Brazil: Biblioteca Digital Brasileira de Computação.
• Freitas L. JACK: A process algebra implementation in Java [Masters Thesis]. Universidade Federal de Pernambuco, Brazil: Centro de Informática, 2002.
• Freitas L, Cavalcanti ALC, Moura H. Animating CSPm using Action Semantics. In: 4th Brazilian Workshop on Formal Methods. 2001, Campina Grande, Brazil: Sociedade Brasileira de Computacao.