Introduction

I am interested in formal specification and verification of critical systems. In particular, the use of theorem provers and modelling tools. I also participate in the Grand Challenge in Software Verification. 

Since 2014, I've been involved in the dependability and design of safety critical medical devices. 

Research Interests

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

• Freitas L, Jones CB. Learning from an expert's proof: AI4FM. In: UV10 (Usable Verification). 2010, Redmond, Washington, USA.
• 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.
• 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.
• 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.
• 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.
• 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.
• Freitas L, McDermott J. Formal methods for security in the Xenon hypervisor. International Journal on Software Tools Technology Transfer 2011, 13(5), 463-489.
• 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.
• 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.
• 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.
• 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. Can a system learn from interactive proofs?. In: HOWARD-60. A Festschrift on the Occasion of Howard Barringer's 60th Birthday. 2014, EasyChair.
• 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. 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.
• 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.
• 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.