About
Associate Professor
Department of Lenguajes, Sistemas Informáticos e Ingeniería de Software
Escuela Técnica Superior de Ingenieros en Informática
Universidad Politécnica de Madrid
 Office: 2304
 Phone: +34 91 067 29 97
 Scopus ID: 37003104900
 DBLP: DBLP Record
 Research Groups: COSTA and BABEL
 Email: guillermo.roman (at) upm.es
 City: Boadilla del Monte
 ORCID: https://orcid.org/0000000254278855
 Google Scholar: Google Profile
Teaching Activities
EIT Digital Master Human Computer Interaction and Design
 Programming of User Interfaces
Interuniversity Master Degree in Formal Methods in Computer Science
 Analysis of Concurrent and Distributed Systems
Bachelor Degree in Computer Engineering
 Programming Project
 Concurrencia
 Algoritmos y Estructura de Datos
 Programación para Sistemas
 Programación II
 Programación I
Research Projects
 Razonamiento Formal para Tecnologías Facilitadoras y Emergentes. From 1/1/2019 to 30/09/2022. Funded by Ministerio de Economía y Competitividad [RTI2018094403BC31]
 BLOQUES  Contratos Inteligentes y Blockchains Escalables y Seguros mediante Verificación y Análisis. From 1/10/2019 to 1/10/2022. Funded by Comunidad de Madrid [S2018/TCS4339]
 SICOMORoCM  SIstemas COnfiables mediante Modelos y herRamientas avanzadas. From 1/10/2014 to 1/10/2018. Funded by Comunidad de Madrid [S2013/ICE3006]
 LOBASS  SIstemas COnfiables mediante Modelos y herRamientas avanzadas. From 1/10/2014 to 1/10/2018. Funded by Ministerio de Economía y Competitividad [S2013/ICE3006]
 ENVISAGE  Engineering Virtualized Services. From 1/10/2013 until 1/10/2016. Funded by EU under FP7 [FP7ICT610582]
 VIVAC  Validation and Verification of Concurrent Applications. From 1/1/2013 to 31/12/205. Funded by Ministerio de Economiía y Competitividad, España [TIN201238137]
 DOVES  Development Of Verifiable and Efficient Software. From 1/1/2009 to 31/12/2013. Funded by Ministerio de Educación y Ciencia, España [MEC 200805624/TIN]
 HATS  Highly Adaptable and Trustworthy Software using Formal Methods. From 1/3/2009 to 28/2/2013). Funded by the EU Commission [EU IST FET Programme. Integrated Project. Grant agreement #231620]
Curriculum Vitae
Education
Informatics Engineer (2004)
E.T.S. de Ingenieros en Informática, Unversidad Politécnica de Madrid
Master in Information Technologies (2007)
E.T.S. de Ingenieros en Informática, Unversidad Politécnica de Madrid
PhD in Software and Systems (2012)
E.T.S. de Ingenieros en Informática, Unversidad Politécnica de Madrid
Professional Experience
Analyst and Programmer (2004)
Telefonica Soluciones
Analyst (20052006)
TSystems
Project Manager (20072009)
First Data Ibérica
Academic Experience
Adjunct Professor
2007  2009
E.T.S. de Ingenieros en Informática, Unversidad Politécnica de Madrid
Research Project Technician
2010  2014
E.T.S. de Ingenieros en Informática, Unversidad Politécnica de Madrid
Postdoc Researcher
2014  2015
E.T.S. de Ingenieros en Informática, Unversidad Politécnica de Madrid
Assistant Professor
2016  2020
E.T.S. de Ingenieros en Informática, Unversidad Politécnica de Madrid
Associate Professor
2020  ...
E.T.S. de Ingenieros en Informática, Unversidad Politécnica de Madrid
Publications
International Journals
[1] 
Elvira Albert, Jesús Correas, Pablo Gordillo, Guillermo RománDíez, and
Albert Rubio.
Don't Run on Fumes  Parametric Gas Bounds for Smart Contracts.
Journal of Systems and Software, 176:110923, 2021.
[ bibtex 
abstract 
DOI 
PDF ]

[2] 
Cosimo Laneve, Michael Lienhardt, Ka I Pun, and Guillermo
RománDíez.
Time analysis of actor programs.
Journal of Logical and Algebraic Methods in Programming, 105:1
 27, 2019.
[ bibtex 
abstract 
DOI ]

[3] 
Elvira Albert, Jesús Correas, and Guillermo RománDíez.
Peak Resource Analysis of Concurrent Distributed Systems.
Journal of Systems and Software, 149:35  62, 2019.
[ bibtex 
abstract 
DOI ]

[4] 
Elvira Albert, Jesús Correas, Einar Broch Johnsen Ka I Pun, and Guillermo RománDíez.
Parallel Cost Analysis.
ACM Transactions on Computational Logic, 19(4):1  37, 2018.
[ bibtex 
abstract 
DOI ]

[5] 
Elvira Albert, Richard Bubel, Samir Genaim, Reiner Hähnle, Germán Puebla,
and Guillermo RománDíez.
A Formal Verification Framework for Static Analysis.
Software and Systems Modeling, 15(4):9871012, 2016.
[ bibtex 
abstract 
DOI 
PDF 
http ]

[6] 
Elvira Albert, Puri
Arenas, Jesús Correas, Samir Genaim, Miguel GómezZamalloa, and Germán Puebla an d Guillermo RománDíez.
ObjectSensitive Cost Analysis for Concurrent Objects.
Software Testing, Verification and Reliability, 25(3):218271,
2015.
[ bibtex 
abstract 
DOI 
PDF 
http ]

[7] 
Elvira Albert, Jesús Correas, Germán Puebla, and Guillermo RománDíez.
Quantified Abstract Configurations of Distributed Systems.
Formal Aspects of Computing, 27(4):665699, 2015.
[ bibtex 
abstract 
DOI 
PDF 
http ]

[8] 
Elvira Albert, Jesús Correas, Germán Puebla, and Guillermo RománDíez.
A MultiDomain Incremental Analysis Engine and its
Application to Incremental Resource Analysis.
Theoretical Computer Science, 585(0):91  114, 2015.
[ bibtex 
abstract 
DOI 
PDF 
http ]

[9] 
Elvira Albert, Puri
Arenas, Samir Genaim, Germán Puebla, and Guillermo RománDíez.
Conditional Termination of Loops over Heapallocated Data.
Science of Computer Programming, 92:2  24, 2014.
[ bibtex 
abstract 
DOI 
PDF 
http ]

International Conferences
[1] 
Elvira Albert, Jesús Correas, Pablo Gordillo, Guillermo RománDíez, and
Albert Rubio.
GASOL: Gas Analysis and Optimization for Ethereum Smart
Contracts.
In Armin Biere and David Parker, editors, 26th International
Conference on Tools and Algorithms for the Construction and Analysis of
Systems, TACAS 2020. Proceedings, volume 12079 of Lecture Notes in
Computer Science, pages 118125. Springer, 2020.
[ bibtex 
abstract 
DOI 
PDF ]

[2]  Elvira Albert, Jesús Correas, Pablo Gordillo, Guillermo RománDíez, and Albert Rubio. Smart, and also reliable and gasefficient, contracts. In 13th IEEE International Conference on Software Testing, Validation and Verification, ICST 2020. Proceedings, IEEE, 2020. [ bibtex  abstract  DOI  PDF ] 
[3] 
Elvira Albert, Jesús Correas, Pablo Gordillo, Guillermo RománDíez, and
Albert Rubio.
SAFEVM: A Safety Verifier for Ethereum Smart Contracts.
In Dongmei Zhang and Anders Møller, editors, ACM SIGSOFT
International Symposium on Software Testing and Analysis, ISSTA 2019.
Proceedings, ACM, pages 386389, 2019.
[ bibtex 
abstract 
DOI 
PDF ]

[4]  Elvira Albert, Puri Arenas, Jesús Correas, Samir Genaim, Miguel GómezZamalloa, Enrique MartinMartin, Germán Puebla, and Guillermo RománDíez. Resource Analysis: From Sequential to Concurrent and Distributed Programs. In Nikolaj Bjørner and Frank D. de Boer, editors, FM 2015: Formal Methods  20th International Symposium, Oslo, Norway, June 2426, 2015, Proceedings, volume 9109 of Lecture Notes in Computer Science, pages 317. Springer, 2015. [ bibtex  abstract  DOI  PDF  http ] 
[5] 
Elvira Albert, Jesús Correas, Einar Broch Johnsen, and Guillermo RománDíez.
Parallel Cost Analysis of Distributed Systems.
In Static Analysis  22nd International Symposium, SAS 2015.
Proceedings, volume 9291 of Lecture Notes in Computer Science, pages
275292. Springer, 2015.
[ bibtex 
abstract 
DOI 
PDF 
http ]

[6] 
Elvira Albert, Jesús Correas, and Guillermo RománDíez.
NonCumulative Resource Analysis.
In Proceedings of 21st International Conference on Tools and
Algorithms for the Construction and Analysis of Systems (TACAS 2015), volume
9035 of Lecture Notes in Computer Science, pages 85100. Springer,
2015.
[ bibtex 
abstract 
DOI 
PDF 
http ]

[7] 
Elvira Albert, Jesús Correas, Enrique
MartínMartín, and Guillermo
RománDíez.
Static Inference of Transmission Data Sizes in
Distributed Systems.
In 6th International Symposium On Leveraging Applications of
Formal Methods, Verification and Validation (ISOLA'14), volume 8803 of
Lecture Notes in Computer Science, pages 104119. Springer, 2014.
[ bibtex 
abstract 
DOI 
PDF 
http ]

[8] 
Elvira Albert, Jesús Correas, and Guillermo RománDíez.
Peak Cost Analysis of Distributed Systems.
In Markus MüllerOlm and Helmut Seidl, editors, Static
Analysis  21st International Symposium, SAS 2014, Munich, Germany,
September 1113, 2014. Proceedings, volume 8723 of Lecture Notes in
Computer Science, pages 1833. Springer, 2014.
[ bibtex 
abstract 
DOI 
PDF 
http ]

[9] 
Elvira Albert, Puri
Arenas, Antonio FloresMontoya, Samir Genaim, Miguel GómezZamalloa, Enrique MartinMartin, Germán Puebla, and Guillermo RománDíez.
SACO: Static Analyzer for Concurrent Objects.
In Erika Ábrahám and Klaus Havelund, editors, Tools and
Algorithms for the Construction and Analysis of Systems  20th International
Conference, TACAS 2014, volume 8413 of Lecture Notes in Computer
Science, pages 562567. Springer, 2014.
[ bibtex 
abstract 
DOI 
PDF 
http ]

[10] 
Elvira Albert, Jesús Correas, Germán Puebla, and Guillermo RománDíez.
Quantified Abstractions of Distributed Systems.
In 10th International Conference on integrated Formal Methods
(iFM'13), volume 7940 of Lecture Notes in Computer Science, pages
285300. Springer, June 2013.
[ bibtex 
abstract 
DOI 
PDF 
http ]

[11] 
Elvira Albert, Richard Bubel, Samir Genaim, Reiner Hähnle, and Guillermo RománDíez.
Verified Resource Guarantees for Heap Manipulating
Programs.
In Proceedings of the 15th International Conference on
Fundamental Approaches to Software Engineering, FASE 2012, Tallinn, Estonia,
March, 2012, volume 7212 of Lecture Notes in Computer Science, pages
130145. Springer, March 2012.
[ bibtex 
abstract 
DOI 
PDF 
http ]

[12] 
Elvira Albert, Jesús Correas, Germán Puebla, and Guillermo RománDíez.
Incremental Resource Usage Analysis.
In Proceedings of the 2012 ACM SIGPLAN Workshop on Partial
Evaluation and Program Manipulation, PEPM 2012, Philadelphia, Pennsylvania,
USA, January 2324, 2012, pages 2534. ACM Press, January 2012.
[ bibtex 
abstract 
DOI 
PDF 
http ]

[13] 
Elvira Albert, Jesús Correas, Germán Puebla, and Guillermo RománDíez.
Towards Incremental Resource Usage Analysis.
In The Ninth Asian Symposium on Programming Languages and
Systems (APLAS'11), December 2011.
Poster Presentation.
[ bibtex 
abstract 
PDF ]

[14] 
Elvira Albert, Richard Bubel, Samir Genaim, Reiner Hähnle, Germán Puebla,
and Guillermo RománDíez.
Verified Resource Guarantees using COSTA and KeY.
In SiauCheng Khoo and Jeremy G. Siek, editors, Proceedings of
the 2011 ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation,
PEPM 2011, Austin, TX, USA, January 2425, 2011, SIGPLAN, pages 7376. ACM,
2011.
[ bibtex 
abstract 
DOI 
DOI 
PDF ]

[15] 
Elvira Albert, Puri
Arenas, Samir Genaim, Miguel GómezZamalloa, Germán Puebla, Diana Ramirez, Guillermo RománDíez, and Damiano Zanardini.
Termination and Cost Analysis with COSTA and its User
Interfaces.
In Spanish Conference on Programming and Computer Languages
(PROLE'09), volume 258 of Electronic Notes in Theoretical Computer
Science, pages 109121. Elsevier, September 2009.
[ bibtex 
abstract 
DOI 
PDF ]

Publication in Workshops
[1] 
Elvira Albert, Samir Genaim, and Guillermo RománDíez.
Conditional Termination of Loops over Arrays.
In Proceedings of the Bytecode 2012 workshop, the Seventh
Workshop on Bytecode Semantics, Verification, Analysis and Transformation
(Bytecode 2012), March 2012.
[ bibtex 
abstract ]

[2] 
Elvira Albert, Richard Bubel, Samir Genaim, Reiner Hähnle, and Guillermo RománDíez.
Verified Resource Guarantees for Heap Manipulating
Programs.
In 10th KeY Symposium 2011, August 2011.
[ bibtex 
abstract 
PDF ]

Books
[1]  Elvira Albert, Jesús Correas, and Guillermo RománDíez. Resource Analysis of Distributed Systems. In Theory and Practice of Formal Methods  Essays Dedicated to Frank de Boer on the Occasion of His 60th Birthday, pages 3346. Springer, 2016. [ bibtex  abstract  DOI  http ] 
[2] 
Elvira Albert, Diego Esteban Alonso Blas, Puri Arenas, Jesús Correas, Antonio
FloresMontoya, Samir Genaim, Miguel GómezZamalloa, Abu Naser Masud,
Germán Puebla, José Miguel Rojas, Guillermo RománDíez, and Damiano Zanardini.
Automatic Inference of Bounds on Resource Consumption.
In Formal Methods for Components and Objects  11th
International Symposium, FMCO 2012, Bertinoro, Italy, September 2428, 2012,
Revised Lectures, volume 7866 of Lecture Notes in Computer Science,
pages 119144. Springer, 2013.
[ bibtex 
abstract 
DOI 
PDF 
http ]
