Search

Your search keyword '"Freitas, Leo"' showing total 117 results
Start Over Author "Freitas, Leo"
117 results on '"Freitas, Leo"'

1. International System of Quantities library in VDM

Author

Freitas, Leo

Subjects
Computer Science - Software Engineering
Abstract

The International Systems of Quantities (ISQ) standard was published in 1960 to tame the wide diversity of measurement systems being developed across the world, such as the centimetre-gram-second versus the meter-kilogram-second for example. Such a standard is highly motivated by the potential of ``trivial'' (rather error-prone) mistakes in converting between incompatible units. There have been such accidents in space missions, medical devices, etc. Thus, rendering modelling or simulation experiments unusable or unsafe. We address this problem by providing a \textbf{SAFE}-ISQ VDM-library that is: Simple, Accurate, Fast, and Effective. It extends an ecosystem of other VDM mathematical toolkit extensions, which include a translation and proof environment for VDM in Isabelle at https://github.com/leouk/VDM_Toolkit., Comment: 14 pages,, 1 figure, 21st Overture Workshop, Lubeck 2023

Published
2023

2. Topologically sorting VDM-SL definitions for Isabelle/HOL translation

Author

Freitas, Leo

Subjects
Computer Science - Programming Languages
Abstract

There is an ecosystem of VDM libraries and extensions that includes a translation and proof environment for VDM in Isabelle. Translation works for a large subset of VDM-SL and further constructs are being added on demand. A key impediment for novice users is that Isabelle/HOL requires all definitions to be declared before they are used, where (mutually) recursive definitions must be defined in tandem. In this paper, we describe a solution to this problem, which will enable wider access to the translator plugin for novice users as well as real models.

Published
2023

3. SmartAudits: Applying Timebands to a Medical Device

Author

Freitas, Leo, Buhagiar, Aaron John, Scott III, William E., Goos, Gerhard, Series Editor, Hartmanis, Juris, Founding Editor, Bertino, Elisa, Editorial Board Member, Gao, Wen, Editorial Board Member, Steffen, Bernhard, Editorial Board Member, Yung, Moti, Editorial Board Member, Cavalcanti, Ana, editor, and Baxter, James, editor

Published
2024
Full Text
View/download PDF

4. Verification Technology for VDM: Craft and Automation

Author

Fitzgerald, John, Larsen, Peter Gorm, Pierce, Ken, Freitas, Leo, Battle, Nick, Goos, Gerhard, Series Editor, Hartmanis, Juris, Founding Editor, Bertino, Elisa, Editorial Board Member, Gao, Wen, Editorial Board Member, Steffen, Bernhard, Editorial Board Member, Yung, Moti, Editorial Board Member, Cavalcanti, Ana, editor, and Baxter, James, editor

Published
2024
Full Text
View/download PDF

5. VDM recursive functions in Isabelle/HOL

Author

Freitas, Leo and Larsen, Peter Gorm

Subjects
Computer Science - Formal Languages and Automata Theory
Abstract

For recursive functions general principles of induction needs to be applied. Instead of verifying them directly using the Vienna Development Method Specification Language (VDM-SL), we suggest a translation to Isabelle/HOL. In this paper, the challenges of such a translation for recursive functions are presented. This is an extension of an existing translation and a VDM mathematical toolbox in Isabelle/HOL enabling support for recursive functions.

Published
2023

6. Specification-based CSV Support in VDM

Author

Freitas, Leo and Buhagiar, Aaron John

Subjects
Computer Science - Software Engineering, Computer Science - Programming Languages
Abstract

CSV is a widely used format for data representing systems control, information exchange and processing, logging, etc. Nevertheless, the format is riddled with tricky corner cases and inconsistencies, which can make input data unreliable, thus, rendering modelling or simulation experiments unusable or unsafe. We address this problem by providing a SAFE-CSV VDM-library that is: Simple, Accurate, Fast, and Effective. It extends an ecosystem of other VDM mathematical toolkit extensions, which also includes a translation and proof environment for VDM in Isabelle, Comment: 12 pages, 2 figures, submitted to 21st Overture workshop

Published
2023

7. Security Analysis of the Open Banking Account and Transaction API Protocol

Author

Almehrej, Abdulaziz, Freitas, Leo, and Modesti, Paolo

Subjects
Computer Science - Cryptography and Security
Abstract

To counteract the lack of competition and innovation in the financial services industry, the EU has issued the Second Payment Services Directive (PSD2) encouraging account servicing payment service providers to share data. The UK, similarly to other European countries, has promoted a standard API for data sharing:~the Open Banking Standard. We present a formal security analysis of its APIs, focusing on the correctness of the Account and Transaction API protocol. The work relies on a previously proposed methodology, which provided a practical approach to protocol modelling and verification., Comment: 18 pages, 2 figures

Published
2020

8. Digital Twins for Organ Preservation Devices

Author

Buhagiar, Aaron John, Freitas, Leo, Scott III, William E., Larsen, Peter Gorm, Goos, Gerhard, Founding Editor, Hartmanis, Juris, Founding Editor, Bertino, Elisa, Editorial Board Member, Gao, Wen, Editorial Board Member, Steffen, Bernhard, Editorial Board Member, Yung, Moti, Editorial Board Member, and Margaria, Tiziana, editor

Published
2022
Full Text
View/download PDF

9. Account and Transaction Protocol of the Open Banking Standard

Author

Almehrej, Abdulaziz, Freitas, Leo, Modesti, Paolo, Goos, Gerhard, Founding Editor, Hartmanis, Juris, Founding Editor, Bertino, Elisa, Editorial Board Member, Gao, Wen, Editorial Board Member, Steffen, Bernhard, Editorial Board Member, Woeginger, Gerhard, Editorial Board Member, Yung, Moti, Editorial Board Member, Raschke, Alexander, editor, Méry, Dominique, editor, and Houdek, Frank, editor

Published
2020
Full Text
View/download PDF

10. VDM at Large: Modelling the EMV® Generation Kernel

Author

Freitas, Leo, Hutchison, David, Series Editor, Kanade, Takeo, Series Editor, Kittler, Josef, Series Editor, Kleinberg, Jon M., Series Editor, Mattern, Friedemann, Series Editor, Mitchell, John C., Series Editor, Naor, Moni, Series Editor, Pandu Rangan, C., Series Editor, Steffen, Bernhard, Series Editor, Terzopoulos, Demetri, Series Editor, Tygar, Doug, Series Editor, Weikum, Gerhard, Series Editor, Massoni, Tiago, editor, and Mousavi, Mohammad Reza, editor

Published
2018
Full Text
View/download PDF

11. A Methodology for Protocol Verification Applied to EMV® 1

Author

Freitas, Leo, Modesti, Paolo, Emms, Martin, Hutchison, David, Series Editor, Kanade, Takeo, Series Editor, Kittler, Josef, Series Editor, Kleinberg, Jon M., Series Editor, Mattern, Friedemann, Series Editor, Mitchell, John C., Series Editor, Naor, Moni, Series Editor, Pandu Rangan, C., Series Editor, Steffen, Bernhard, Series Editor, Terzopoulos, Demetri, Series Editor, Tygar, Doug, Series Editor, Weikum, Gerhard, Series Editor, Massoni, Tiago, editor, and Mousavi, Mohammad Reza, editor

Published
2018
Full Text
View/download PDF

13. An Axiomatic Value Model for Isabelle/UTP

Author

Zeyda, Frank, Foster, Simon, Freitas, Leo, Hutchison, David, Series editor, Kanade, Takeo, Series editor, Kittler, Josef, Series editor, Kleinberg, Jon M., Series editor, Mattern, Friedemann, Series editor, Mitchell, John C., Series editor, Naor, Moni, Series editor, Pandu Rangan, C., Series editor, Steffen, Bernhard, Series editor, Terzopoulos, Demetri, Series editor, Tygar, Doug, Series editor, Weikum, Gerhard, Series editor, Bowen, Jonathan P., editor, and Zhu, Huibiao, editor

Published
2017
Full Text
View/download PDF

14. Modelling and Verifying a Priority Scheduler for an SCJ Runtime Environment

Author

Freitas, Leo, Baxter, James, Cavalcanti, Ana, Wellings, Andy, Hutchison, David, Series editor, Kanade, Takeo, Series editor, Kittler, Josef, Series editor, Kleinberg, Jon M., Series editor, Mattern, Friedemann, Series editor, Mitchell, John C., Series editor, Naor, Moni, Series editor, Pandu Rangan, C., Series editor, Steffen, Bernhard, Series editor, Terzopoulos, Demetri, Series editor, Tygar, Doug, Series editor, Weikum, Gerhard, Series editor, Ábrahám, Erika, editor, and Huisman, Marieke, editor

Published
2016
Full Text
View/download PDF

15. A Model for Capturing and Replaying Proof Strategies

Author

Freitas, Leo, Jones, Cliff B., Velykis, Andrius, Whiteside, Iain, Hutchison, David, Series editor, Kanade, Takeo, Series editor, Kittler, Josef, Series editor, Kleinberg, Jon M., Series editor, Mattern, Friedemann, Series editor, Mitchell, John C., Series editor, Naor, Moni, Series editor, Pandu Rangan, C., Series editor, Steffen, Bernhard, Series editor, Terzopoulos, Demetri, Series editor, Tygar, Doug, Series editor, Weikum, Gerhard, Series editor, Giannakopoulou, Dimitra, editor, and Kroening, Daniel, editor

Published
2014
Full Text
View/download PDF

16. Proof Patterns for Formal Methods

Author

Freitas, Leo, Whiteside, Iain, Hutchison, David, editor, Kanade, Takeo, editor, Kittler, Josef, editor, Kleinberg, Jon M., editor, Kobsa, Alfred, editor, Mattern, Friedemann, editor, Mitchell, John C., editor, Naor, Moni, editor, Nierstrasz, Oscar, editor, Pandu Rangan, C., editor, Steffen, Bernhard, editor, Terzopoulos, Demetri, editor, Tygar, Doug, editor, Weikum, Gerhard, editor, Jones, Cliff, editor, Pihlajasaari, Pekka, editor, and Sun, Jun, editor

Published
2014
Full Text
View/download PDF

18. Ours Is to Reason Why

Author

Jones, Cliff B., Freitas, Leo, Velykis, Andrius, Hutchison, David, Series editor, Kanade, Takeo, Series editor, Kittler, Josef, Series editor, Kleinberg, Jon M., Series editor, Mattern, Friedemann, Series editor, Mitchell, John C., Series editor, Naor, Moni, Series editor, Nierstrasz, Oscar, Series editor, Pandu Rangan, C., Series editor, Steffen, Bernhard, Series editor, Sudan, Madhu, Series editor, Terzopoulos, Demetri, Series editor, Tygar, Doug, Series editor, Vardi, Moshe Y., Series editor, Weikum, Gerhard, Series editor, Liu, Zhiming, editor, Woodcock, Jim, editor, and Zhu, Huibiao, editor

Published
2013
Full Text
View/download PDF

19. Advanced VDM Support in Visual Studio Code

Author

Rask, Jonas Kjær, Madsen, Frederik Palludan, Battle, Nick, Freitas, Leo, Macedo, Hugo Daniel, Larsen, Peter Gorm, Macedo, Hugo Daniel, and Pierce, Ken

Published
2022

20. Formal Modelling of Separation Kernel Components

Author

Velykis, Andrius, Freitas, Leo, Hutchison, David, editor, Kanade, Takeo, editor, Kittler, Josef, editor, Kleinberg, Jon M., editor, Mattern, Friedemann, editor, Mitchell, John C., editor, Naor, Moni, editor, Nierstrasz, Oscar, editor, Pandu Rangan, C., editor, Steffen, Bernhard, editor, Sudan, Madhu, editor, Terzopoulos, Demetri, editor, Tygar, Doug, editor, Vardi, Moshe Y., editor, Weikum, Gerhard, editor, Cavalcanti, Ana, editor, Deharbe, David, editor, Gaudel, Marie-Claude, editor, and Woodcock, Jim, editor

Published
2010
Full Text
View/download PDF

21. UTP and Temporal Logic Model Checking

Author

Anderson, Hugh, Ciobanu, Gabriel, Freitas, Leo, Hutchison, David, editor, Kanade, Takeo, editor, Kittler, Josef, editor, Kleinberg, Jon M., editor, Mattern, Friedemann, editor, Mitchell, John C., editor, Naor, Moni, editor, Nierstrasz, Oscar, editor, Pandu Rangan, C., editor, Steffen, Bernhard, editor, Sudan, Madhu, editor, Terzopoulos, Demetri, editor, Tygar, Doug, editor, Vardi, Moshe Y., editor, Weikum, Gerhard, editor, and Butterfield, Andrew, editor

Published
2010
Full Text
View/download PDF

22. Mechanising Data-Types for Kernel Design in Z

Author

Freitas, Leo, Hutchison, David, editor, Kanade, Takeo, editor, Kittler, Josef, editor, Kleinberg, Jon M., editor, Mattern, Friedemann, editor, Mitchell, John C., editor, Naor, Moni, editor, Nierstrasz, Oscar, editor, Pandu Rangan, C., editor, Steffen, Bernhard, editor, Sudan, Madhu, editor, Terzopoulos, Demetri, editor, Tygar, Doug, editor, Vardi, Moshe Y., editor, Weikum, Gerhard, editor, Oliveira, Marcel Vinícius Medeiros, editor, and Woodcock, Jim, editor

Published
2009
Full Text
View/download PDF

24. Proving Theorems About JML Classes

Author

Freitas, Leo, Woodcock, Jim, Hutchison, David, editor, Kanade, Takeo, editor, Kittler, Josef, editor, Kleinberg, Jon M., editor, Mattern, Friedemann, editor, Mitchell, John C., editor, Naor, Moni, editor, Nierstrasz, Oscar, editor, Pandu Rangan, C., editor, Steffen, Bernhard, editor, Sudan, Madhu, editor, Terzopoulos, Demetri, editor, Tygar, Doug, editor, Vardi, Moshe Y., editor, Weikum, Gerhard, editor, Jones, Cliff B., editor, Liu, Zhiming, editor, and Woodcock, Jim, editor

Published
2007
Full Text
View/download PDF

25. Z/Eves and the Mondex Electronic Purse

Author

Woodcock, Jim, Freitas, Leo, Hutchison, David, editor, Kanade, Takeo, editor, Kittler, Josef, editor, Kleinberg, Jon M., editor, Mattern, Friedemann, editor, Mitchell, John C., editor, Naor, Moni, editor, Nierstrasz, Oscar, editor, Pandu Rangan, C., editor, Steffen, Bernhard, editor, Sudan, Madhu, editor, Terzopoulos, Demetri, editor, Tygar, Dough, editor, Vardi, Moshe Y., editor, Weikum, Gerhard, editor, Barkaoui, Kamel, editor, Cavalcanti, Ana, editor, and Cerone, Antonio, editor

Published
2006
Full Text
View/download PDF

26. Taking Our Own Medicine: Applying the Refinement Calculus to State-Rich Refinement Model Checking

Author

Freitas, Leo, Cavalcanti, Ana, Woodcock, Jim, Hutchison, David, editor, Kanade, Takeo, editor, Kittler, Josef, editor, Kleinberg, Jon M., editor, Mattern, Friedemann, editor, Mitchell, John C., editor, Naor, Moni, editor, Nierstrasz, Oscar, editor, Pandu Rangan, C., editor, Steffen, Bernhard, editor, Sudan, Madhu, editor, Terzopoulos, Demetri, editor, Tygar, Dough, editor, Vardi, Moshe Y., editor, Weikum, Gerhard, editor, Liu, Zhiming, editor, and He, Jifeng, editor

Published
2006
Full Text
View/download PDF

27. CZT Support for Z Extensions

Author

Miller, Tim, Freitas, Leo, Malik, Petra, Utting, Mark, Hutchison, David, editor, Kanade, Takeo, editor, Kittler, Josef, editor, Kleinberg, Jon M., editor, Mattern, Friedemann, editor, Mitchell, John C., editor, Naor, Moni, editor, Nierstrasz, Oscar, editor, Pandu Rangan, C., editor, Steffen, Bernhard, editor, Sudan, Madhu, editor, Terzopoulos, Demetri, editor, Tygar, Dough, editor, Vardi, Moshe Y., editor, Weikum, Gerhard, editor, Romijn, Judi, editor, Smith, Graeme, editor, and van de Pol, Jaco, editor

Published
2005
Full Text
View/download PDF

41. GENERAL NOTES

Author

DE FREITAS, LEO J., STEWART, ANGUS, and ADAMS, SALLY

Published
1985

Catalog

Books, media, physical & digital resources
See catalog results