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

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

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)

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 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)

Security Analysis of Smart Grids. - Joaquín Márquez; Gabriel Rodríguez; Gustavo Betarte; Juan Diego Campo; Eduardo Grampín (SSN, 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)

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)

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)

Proximity tracing applications for COVID-19: data privacy and security. - Gustavo Betarte; Juan Diego Campo; Andrea Delgado 001; Pablo Ezzatti; Laura González 001; Álvaro Martín; Rodrigo Martínez; Bárbara Muracciole (CLEI, 2021)

Contact tracing solutions for COVID-19: applications, data privacy and security. - Gustavo Betarte; Juan Diego Campo; Andrea Delgado 001; Laura González 001; Álvaro Martín; Rodrigo Martínez; Bárbara Muracciole (CLEI Electron. J., 2022)

Third-Party Trackers in COVID-19 Mobile Applications Can Enable Privacy Leaks. - Nicolás Serrano; Gustavo Betarte; Juan Diego Campo (LADC, 2023)

Process Mining-Based Assessment of Cyber Range Trainings. - Guillermo Guerrero; Gustavo Betarte; Juan Diego Campo (CLEI, 2024)

COVID-19 Mobile Applications: A Study of Trackers and Data Leaks. - Nicolás Serrano; Gustavo Betarte; Juan Diego Campo (J. Internet Serv. Appl., 2024)