Our experiences teaching functional programming at University of Rio Cuarto (Argentina). - Ariel Ferreira Szpiniak; Carlos Daniel Luna; Ricardo H. Medel (ACM SIGCSE Bull., 1998)

Una Generalizacion del Modelo AGM de Cambio de Creencias. - Carlos Daniel Luna (Inteligencia Artif., 2001)

Especificación y Análisis de Sistemas de Tiempo Real en Teoría de Tipos. - Carlos Daniel Luna (Computación y Sistemas, 2004)

A Formal Specification of the MIDP 2.0 Security Model. - Santiago Zanella-Béguelin; Gustavo Betarte; Carlos Luna 001 (Formal Aspects in Security and Trust, 2006)

Behavior Specification of Product Lines via Feature Models and UML Statecharts with Variabilities. - Ariel Gonzalez; Carlos Luna 001 (SCCC, 2008)

A Framework for the Analysis of Access Control Models for Interactive Mobile Devices. - Juan Manuel Crespo; Gustavo Betarte; Carlos Luna 001 (TYPES, 2008)

Formal Specification and Analysis of the MIDP 3.0 Security Model. - Gustavo Mazeikis; Gustavo Betarte; Carlos Luna 001 (SCCC, 2009)

A Certified Access Controller for JME-MIDP 2.0 Enabled Mobile Devices. - Ramin Roushani Oskui; Gustavo Betarte; Carlos Luna 001 (SCCC, 2009)

Specification of Products and Product Lines - Ariel Gonzalez; Carlos Luna 001 (WRS, 2009)

A Type-Theoretic Framework for Certified Model Transformations. - Daniel Calegari; Carlos Luna 001; Nora Szasz; Alvaro Tasistro (SBMF, 2010)

Formally Verifying Isolation and Availability in an Idealized Model of Virtualization. - Gilles Barthe; Gustavo Betarte; Juan Diego Campo; Carlos Luna 001 (FM, 2011)

A Formal Specification of the DNSSEC Model. - Ezequiel Bazan Eixarch; Gustavo Betarte; Carlos Daniel Luna (Electron. Commun. Eur. Assoc. Softw. Sci. Technol., 2011)

Delayed completion of Final Project of the career Computer Analyst: Seeking its causes. - Fabio Zorzan; Mariana Frutos; Ariel Arsaute; Marcela Daniele; Paola Martellotto; Marcelo Uva; Carlos Luna 001 (CLEI, 2012)

Cache-Leakage Resilient OS Isolation in an Idealized Model of Virtualization. - Gilles Barthe; Gustavo Betarte; Juan Diego Campo; Carlos Luna 001 (CSF, 2012)

Alternating-Time Temporal Logic in the Calculus of (Co)Inductive Constructions. - Dante Zanarini; Carlos Luna 001; Luis Sierra (SBMF, 2012)

Automatizacion del Proceso de Instanciacion del Comportamiento de Productos de una Linea de Productos de Software. - Ariel Gonzalez; Fabio Zorzan; Carlos Luna 001; Nora Szasz (CIbSE, 2013)

Formally Verified Implementation of an Idealized Model of Virtualization. - Gilles Barthe; Gustavo Betarte; Juan Diego Campo; Jesús Mauricio Chimento; Carlos Luna 001 (TYPES, 2013)

Metamodel-based transformation from UML state machines to DEVS models. - Ariel Gonzalez; Carlos Daniel Luna; Roque Cuello; Marcela Perez; Marcela Daniele (CLEI, 2014)

Pedagogical Experiences in a Highly Populated Undergraduate Programming Course Teaching How to Develop Medium Size Information Systems. - Lorena Etcheverry; Carlos Luna 001; Libertad Tansini (CLEI Electron. J., 2014)

System-level non-interference for constant-time cryptography. - Gilles Barthe; Gustavo Betarte; Juan Diego Campo; Carlos Luna 001; David Pichardie (IACR Cryptol. ePrint Arch., 2014)

Verifying Android's Permission Model. - Gustavo Betarte; Juan Diego Campo; Carlos Daniel Luna; Agustín Romano (ICTAC, 2015)

Formal Analysis of Security Models for Mobile Devices, Virtualization Platforms, and Domain Name Systems. - Gustavo Betarte; Carlos Luna 001 (CLEI Electron. J., 2015)

Towards an automatic model transformation mechanism from UML state machines to DEVS models. - Ariel Gonzalez; Carlos Luna 001; Marcela Daniele; Roque Cuello; Marcela Perez (CLEI Electron. J., 2015)

UML state machine as modeling language for DEVS formalism. - Ariel Gonzalez; Carlos Daniel Luna; Rodrigo Abella (CLEI, 2016)

Formal Analysis of Android's Permission-Based Security Model, . - Gustavo Betarte; Juan Diego Campo; Carlos Luna 001; Agustín Romano (Sci. Ann. Comput. Sci., 2016)

Towards formal model-based analysis and testing of Android's security mechanisms. - Gustavo Betarte; Juan Diego Campo; Maximiliano Cristiá; Felipe Gorostiaga; Carlos Luna 001; Camila Sanz (CLEI, 2017)

A Certified Reference Validation Mechanism for the Permission Model of Android. - Gustavo Betarte; Juan Diego Campo; Felipe Gorostiaga; Carlos Luna 001 (LOPSTR, 2017)

Mutation Testing for Java Based on Model-Driven Development. - Ariel Gonzalez; Carlos Luna 001; Gonzalo Bressan (CLEI, 2018)

Security in iOS and Android: A Comparative Analysis. - Raul Ignacio Galuppo; Carlos Luna 001; Gustavo Betarte (SCCC, 2018)

A formal approach for the verification of the permission-based security model of Android. - Carlos Luna 001; Gustavo Betarte; Juan Diego Campo; Camila Sanz; Maximiliano Cristiá; Felipe Gorostiaga (CLEI Electron. J., 2018)

Mutants for Metric Temporal Logic Formulas. - Ariel Gonzalez; Maximiliano Cristiá; Carlos Luna 001 (CIbSE, 2019)

System-Level Non-interference of Constant-Time Cryptography. Part I: Model. - Gilles Barthe; Gustavo Betarte; Juan Diego Campo; Carlos Luna 001 (J. Autom. Reason., 2019)

Towards a Formally Verified Implementation of the MimbleWimble Cryptocurrency Protocol. - Gustavo Betarte; Maximiliano Cristiá; Carlos Daniel Luna; Adrián Silveira; Dante Zanarini (ACNS Workshops, 2020)

Towards a Certified Reference Monitor of the Android 10 Permission System. - Guido De Luca; Carlos Luna 001 (TYPES, 2020)

System-Level Non-interference of Constant-Time Cryptography. Part II: Verified Static Analysis and Stealth Memory. - Gilles Barthe; Gustavo Betarte; Juan Diego Campo; Carlos Luna 001; David Pichardie (J. Autom. Reason., 2020)

Privacy-aware blockchain solutions: design and threat analysis. - Fernanda Molina; Gustavo Betarte; Carlos Luna 001 (CIbSE, 2021)

Error Finding in Real-Time Systems using Mutants of Temporal Properties. - Ariel Gonzalez; Maximiliano Cristiá; Carlos Luna 001 (SCCC, 2021)

Design principles for constructing GDPR-compliant blockchain solutions. - Fernanda Molina; Gustavo Betarte; Carlos Daniel Luna (WETSEB@ICSE, 2021)

Set-Based Models for Cryptocurrency Software. - Gustavo Betarte; Maximiliano Cristiá; Carlos Luna 001; Adrián Silveira; Dante Zanarini (CLEI Electron. J., 2021)

A Formal Analysis of the Mimblewimble Cryptocurrency Protocol. - Adrián Silveira; Gustavo Betarte; Maximiliano Cristiá; Carlos Luna 001 (Sensors, 2021)

An Idealized Model for the Formal Security Analysis of the Mimblewimble Cryptocurrency Protocol. - Adrián Silveira; Gustavo Betarte; Maximiliano Cristiá; Carlos Luna 001 (CLEI, 2022)

Introduction to Strategic Planning as a Support Tool at the Beginning of a Computer Career. - Carlos Luna 001 (SCCC, 2023)

A Blockchain based and GDPR-compliant design of a system for digital education certificates. - Fernanda Molina; Gustavo Betarte; Carlos Luna 001 (CLEI Electron. J., 2023)

An Automatically Verified Prototype of the Android Permissions System. - Maximiliano Cristiá; Guido De Luca; Carlos Luna 001 (J. Autom. Reason., 2023)

Analysis of Security Permissions on Android and iOS from a Privacy Perspective. - Carlos Luna 001; Raul Ignacio Galuppo (CLEI, 2024)

Consent validation for personal data access control using ABAC. - Maria Molina; Gustavo Betarte; Carlos Daniel Luna (LADC, 2024)

Preface to the CLEI 2023 Special Issue. - Hernán Astudillo; Carlos Luna 001; José Miguel Rojas (CLEI Electron. J., 2024)

Preface to the CLEI 2023 Special Issue - Volume II. - Hernán Astudillo; Carlos Luna 001; José Miguel Rojas (CLEI Electron. J., 2024)

A Formal Analysis of the Mimblewimble Cryptocurrency Protocol with a Security Approach. - Adrián Silveira; Gustavo Betarte; Carlos Luna 001 (CLEI Electron. J., 2024)

Verification of Quantitative Temporal Properties in RealTime-DEVS. - Ariel Gonzalez; Maximiliano Cristiá; Carlos Daniel Luna (CoRR, 2024)