default search action
Carlos Daniel Luna
Person information
- affiliation: University of the Republic, Montevideo, Uruguay
Other persons with the same name
- Carlos Andrés Luna Vázquez
(aka: Carlos A. Luna, Carlos Luna 0002) — University of Alcalá, Department of Electronics, Alcalá de Henares, Spain
- Carlos Luna 0003 — Technical University of Ambato, Faculty of Health Sciences, Ecuador
Refine list
refinements active!
zoomed in on ?? of ?? records
view refined list in
export refined list as
2020 – today
- 2024
- [j19]Hernán Astudillo, Carlos Luna, José Miguel Rojas
Preface to the CLEI 2023 Special Issue. CLEI Electron. J. 27(2) (2024) - [j18]Adrián Silveira, Gustavo Betarte, Carlos Luna:
A Formal Analysis of the Mimblewimble Cryptocurrency Protocol with a Security Approach. CLEI Electron. J. 27(3) (2024) - [j17]Adrián Silveira, Gustavo Betarte, Carlos Luna:
A Formal Analysis of the Mimblewimble Cryptocurrency Protocol with a Security Approach. CLEI Electron. J. 27(3) (2024) - [j16]Hernán Astudillo, Carlos Luna, José Miguel Rojas
Preface to the CLEI 2023 Special Issue - Volume II. CLEI Electron. J. 27(4) (2024) - [c31]Carlos Luna, Raul Ignacio Galuppo:
Analysis of Security Permissions on Android and iOS from a Privacy Perspective. CLEI 2024: 1-10 - [c30]Maria Molina, Gustavo Betarte, Carlos Daniel Luna:
Consent validation for personal data access control using ABAC. LADC 2024: 30-31 - [i9]Ariel Gonzalez, Maximiliano Cristiá, Carlos Daniel Luna:
Verification of Quantitative Temporal Properties in RealTime-DEVS. CoRR abs/2409.18732 (2024) - 2023
- [j15]Fernanda Molina, Gustavo Betarte, Carlos Luna:
A Blockchain based and GDPR-compliant design of a system for digital education certificates. CLEI Electron. J. 26(1) (2023) - [j14]Maximiliano Cristiá, Guido De Luca, Carlos Luna:
An Automatically Verified Prototype of the Android Permissions System. J. Autom. Reason. 67(2): 17 (2023) - [c29]Carlos Luna:
Introduction to Strategic Planning as a Support Tool at the Beginning of a Computer Career. SCCC 2023: 1-8 - 2022
- [c28]Adrián Silveira, Gustavo Betarte, Maximiliano Cristiá
An Idealized Model for the Formal Security Analysis of the Mimblewimble Cryptocurrency Protocol. CLEI 2022: 1-10 - [i8]Maximiliano Cristiá, Guido De Luca, Carlos Daniel Luna:
An Automatically Verified Prototype of the Android Permissions System. CoRR abs/2209.10278 (2022) - 2021
- [j13]Gustavo Betarte, Maximiliano Cristiá
Set-Based Models for Cryptocurrency Software. CLEI Electron. J. 24(3) (2021) - [j12]Adrián Silveira
A Formal Analysis of the Mimblewimble Cryptocurrency Protocol. Sensors 21(17): 5951 (2021) - [c27]Fernanda Molina, Gustavo Betarte, Carlos Luna:
Privacy-aware blockchain solutions: design and threat analysis. CIbSE 2021: 150-163 - [c26]Ariel Gonzalez, Maximiliano Cristiá
Error Finding in Real-Time Systems using Mutants of Temporal Properties. SCCC 2021: 1-8 - [c25]Fernanda Molina, Gustavo Betarte, Carlos Daniel Luna:
Design principles for constructing GDPR-compliant blockchain solutions. WETSEB@ICSE 2021: 1-8 - [i7]Adrián Silveira, Gustavo Betarte, Maximiliano Cristiá, Carlos Daniel Luna:
A Formal Analysis of the MimbleWimble Cryptocurrency Protocol. CoRR abs/2104.00822 (2021) - 2020
- [j11]Gilles Barthe, Gustavo Betarte, Juan Diego Campo, Carlos Luna
System-Level Non-interference of Constant-Time Cryptography. Part II: Verified Static Analysis and Stealth Memory. J. Autom. Reason. 64(8): 1685-1729 (2020) - [c24]Gustavo Betarte, Maximiliano Cristiá
Towards a Formally Verified Implementation of the MimbleWimble Cryptocurrency Protocol. ACNS Workshops 2020: 3-23 - [c23]Guido De Luca, Carlos Luna:
Towards a Certified Reference Monitor of the Android 10 Permission System. TYPES 2020: 3:1-3:18 - [i6]Fernanda Molina, Gustavo Betarte, Carlos Daniel Luna:
A Blockchain based and GDPR-compliant design of a system for digital education certificates. CoRR abs/2010.12980 (2020) - [i5]Guido De Luca, Carlos Luna:
Towards a certified reference monitor of the Android 10 permission system. CoRR abs/2011.00720 (2020)
2010 – 2019
- 2019
- [j10]Gilles Barthe, Gustavo Betarte
System-Level Non-interference of Constant-Time Cryptography. Part I: Model. J. Autom. Reason. 63(1): 1-51 (2019) - [c22]Ariel Gonzalez, Maximiliano Cristiá, Carlos Luna:
Mutants for Metric Temporal Logic Formulas. CIbSE 2019: 349-362 - [i4]Gustavo Betarte, Maximiliano Cristiá, Carlos Luna, Adrián Silveira, Dante Zanarini:
Towards a formally verified implementation of the MimbleWimble cryptocurrency protocol. CoRR abs/1907.01688 (2019) - [i3]Gustavo Betarte, Maximiliano Cristiá, Carlos Luna, Adrián Silveira, Dante Zanarini:
Set-Based Models for Cryptocurrency Software. CoRR abs/1908.00591 (2019) - 2018
- [j9]Carlos Luna, Gustavo Betarte, Juan Diego Campo, Camila Sanz, Maximiliano Cristiá
A formal approach for the verification of the permission-based security model of Android. CLEI Electron. J. 21(2) (2018) - [c21]Ariel Gonzalez, Carlos Luna, Gonzalo Bressan:
Mutation Testing for Java Based on Model-Driven Development. CLEI 2018: 1-10 - [c20]Raul Ignacio Galuppo, Carlos Luna, Gustavo Betarte:
Security in iOS and Android: A Comparative Analysis. SCCC 2018: 1-8 - 2017
- [c19]Gustavo Betarte, Juan Diego Campo, Maximiliano Cristiá
Towards formal model-based analysis and testing of Android's security mechanisms. CLEI 2017: 1-10 - [c18]Gustavo Betarte, Juan Diego Campo, Felipe Gorostiaga, Carlos Luna:
A Certified Reference Validation Mechanism for the Permission Model of Android. LOPSTR 2017: 271-288 - [i2]Gustavo Betarte, Juan Diego Campo, Felipe Gorostiaga, Carlos Luna:
A certified reference validation mechanism for the permission model of Android. CoRR abs/1709.03652 (2017) - 2016
- [j8]Gustavo Betarte, Juan Diego Campo, Carlos Luna, Agustín Romano:
Formal Analysis of Android's Permission-Based Security Model, . Sci. Ann. Comput. Sci. 26(1): 27-68 (2016) - [c17]Ariel Gonzalez, Carlos Daniel Luna, Rodrigo Abella:
UML state machine as modeling language for DEVS formalism. CLEI 2016: 1-12 - 2015
- [j7]Ariel Gonzalez, Carlos Luna, Marcela Daniele, Roque Cuello, Marcela Perez:
Towards an automatic model transformation mechanism from UML state machines to DEVS models. CLEI Electron. J. 18(2) (2015) - [j6]Gustavo Betarte, Carlos Luna:
Formal Analysis of Security Models for Mobile Devices, Virtualization Platforms, and Domain Name Systems. CLEI Electron. J. 18(3): 3 (2015) - [c16]Gustavo Betarte, Juan Diego Campo, Carlos Daniel Luna, Agustín Romano:
Verifying Android's Permission Model. ICTAC 2015: 485-504 - 2014
- [j5]Lorena Etcheverry, Carlos Luna, Libertad Tansini:
Pedagogical Experiences in a Highly Populated Undergraduate Programming Course Teaching How to Develop Medium Size Information Systems. CLEI Electron. J. 17(3) (2014) - [c15]Gilles Barthe
System-level Non-interference for Constant-time Cryptography. CCS 2014: 1267-1279 - [c14]Ariel Gonzalez, Carlos Daniel Luna, Roque Cuello, Marcela Perez, Marcela Daniele:
Metamodel-based transformation from UML state machines to DEVS models. CLEI 2014: 1-12 - [i1]Gilles Barthe, Gustavo Betarte, Juan Diego Campo, Carlos Luna, David Pichardie:
System-level non-interference for constant-time cryptography. IACR Cryptol. ePrint Arch. 2014: 422 (2014) - 2013
- [c13]Ariel Gonzalez, Fabio Zorzan, Carlos Luna, Nora Szasz:
Automatizacion del Proceso de Instanciacion del Comportamiento de Productos de una Linea de Productos de Software. CIbSE 2013: 99-112 - [c12]Gilles Barthe
Formally Verified Implementation of an Idealized Model of Virtualization. TYPES 2013: 45-63 - 2012
- [c11]Fabio Zorzan, Mariana Frutos, Ariel Arsaute, Marcela Daniele, Paola Martellotto, Marcelo Uva, Carlos Luna:
Delayed completion of Final Project of the career Computer Analyst: Seeking its causes. CLEI 2012: 1-8 - [c10]Gilles Barthe
Cache-Leakage Resilient OS Isolation in an Idealized Model of Virtualization. CSF 2012: 186-197 - [c9]Dante Zanarini, Carlos Luna, Luis Sierra:
Alternating-Time Temporal Logic in the Calculus of (Co)Inductive Constructions. SBMF 2012: 210-225 - 2011
- [j4]Ezequiel Bazan Eixarch, Gustavo Betarte, Carlos Daniel Luna:
A Formal Specification of the DNSSEC Model. Electron. Commun. Eur. Assoc. Softw. Sci. Technol. 48 (2011) - [c8]Gilles Barthe, Gustavo Betarte, Juan Diego Campo, Carlos Luna:
Formally Verifying Isolation and Availability in an Idealized Model of Virtualization. FM 2011: 231-245 - 2010
- [c7]Daniel Calegari
A Type-Theoretic Framework for Certified Model Transformations. SBMF 2010: 112-127
2000 – 2009
- 2009
- [c6]Ramin Roushani Oskui, Gustavo Betarte, Carlos Luna:
A Certified Access Controller for JME-MIDP 2.0 Enabled Mobile Devices. SCCC 2009: 51-58 - [c5]Gustavo Mazeikis, Gustavo Betarte, Carlos Luna:
Formal Specification and Analysis of the MIDP 3.0 Security Model. SCCC 2009: 59-66 - [c4]Ariel Gonzalez, Carlos Luna:
Specification of Products and Product Lines. WRS 2009: 44-55 - 2008
- [c3]Ariel Gonzalez, Carlos Luna:
Behavior Specification of Product Lines via Feature Models and UML Statecharts with Variabilities. SCCC 2008: 32-41 - [c2]Juan Manuel Crespo, Gustavo Betarte, Carlos Luna:
A Framework for the Analysis of Access Control Models for Interactive Mobile Devices. TYPES 2008: 49-63 - 2006
- [c1]Santiago Zanella Béguelin
A Formal Specification of the MIDP 2.0 Security Model. Formal Aspects in Security and Trust 2006: 220-234 - 2004
- [j3]Carlos Daniel Luna:
Especificación y Análisis de Sistemas de Tiempo Real en Teoría de Tipos. Computación y Sistemas 8(1) (2004) - 2001
- [j2]Carlos Daniel Luna:
Una Generalizacion del Modelo AGM de Cambio de Creencias. Inteligencia Artif. 5(13): 23-32 (2001)
1990 – 1999
- 1998
- [j1]Ariel Ferreira Szpiniak, Carlos Daniel Luna, Ricardo H. Medel
Our experiences teaching functional programming at University of Rio Cuarto (Argentina). ACM SIGCSE Bull. 30(2): 28-30 (1998)
Coauthor Index
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
Unpaywalled article links
Add open access links from to the list of external document links (if available).
Privacy notice: By enabling the option above, your browser will contact the API of unpaywall.org to load hyperlinks to open access articles. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Unpaywall privacy policy.
Archived links via Wayback Machine
For web page which are no longer available, try to retrieve content from the of the Internet Archive (if available).
Privacy notice: By enabling the option above, your browser will contact the API of archive.org to check for archived content of web pages that are no longer available. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Internet Archive privacy policy.
Reference lists
Add a list of references from ,
, and
to record detail pages.
load references from crossref.org and opencitations.net
Privacy notice: By enabling the option above, your browser will contact the APIs of crossref.org, opencitations.net, and semanticscholar.org to load article reference information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Crossref privacy policy and the OpenCitations privacy policy, as well as the AI2 Privacy Policy covering Semantic Scholar.
Citation data
Add a list of citing articles from and
to record detail pages.
load citations from opencitations.net
Privacy notice: By enabling the option above, your browser will contact the API of opencitations.net and semanticscholar.org to load citation information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the OpenCitations privacy policy as well as the AI2 Privacy Policy covering Semantic Scholar.
OpenAlex data
Load additional information about publications from .
Privacy notice: By enabling the option above, your browser will contact the API of openalex.org to load additional information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the information given by OpenAlex.
last updated on 2024-12-13 19:11 CET by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by: