Guillermo Román Díez

Associate Professor
Escuela Técnica Superior de Ingenieros en Informática
Universidad Politécnica de Madrid

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

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
Former Courses
  • 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 [RTI2018-094403-B-C31]
  • 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/TCS-4339]
  • SICOMORo-CM - SIstemas COnfiables mediante Modelos y herRamientas avanzadas. From 1/10/2014 to 1/10/2018. Funded by Comunidad de Madrid [S2013/ICE-3006]
  • 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/ICE-3006]
  • ENVISAGE - Engineering Virtualized Services. From 1/10/2013 until 1/10/2016. Funded by EU under FP7 [FP7-ICT-610582]
  • 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 [TIN2012-38137]
  • 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 2008-05624/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 (2005-2006)

T-Systems

Project Manager (2007-2009)

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

Post-doc 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án-Dí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án-Dí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án-Dí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án-Dí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án-Díez. A Formal Verification Framework for Static Analysis. Software and Systems Modeling, 15(4):987-1012, 2016. [ bibtex | abstract | DOI | PDF | http ]

[6] Elvira Albert, Puri Arenas, Jesús Correas, Samir Genaim, Miguel Gómez-Zamalloa, and Germán Puebla an d Guillermo Román-Díez. Object-Sensitive Cost Analysis for Concurrent Objects. Software Testing, Verification and Reliability, 25(3):218-271, 2015. [ bibtex | abstract | DOI | PDF | http ]

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

[8] Elvira Albert, Jesús Correas, Germán Puebla, and Guillermo Román-Díez. A Multi-Domain 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án-Díez. Conditional Termination of Loops over Heap-allocated 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án-Dí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 118-125. Springer, 2020. [ bibtex | abstract | DOI | PDF ]

[2] Elvira Albert, Jesús Correas, Pablo Gordillo, Guillermo Román-Díez, and Albert Rubio. Smart, and also reliable and gas-efficient, 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án-Dí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 386-389, 2019. [ bibtex | abstract | DOI | PDF ]

[4] Elvira Albert, Puri Arenas, Jesús Correas, Samir Genaim, Miguel Gómez-Zamalloa, Enrique Martin-Martin, Germán Puebla, and Guillermo Román-Dí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 24-26, 2015, Proceedings, volume 9109 of Lecture Notes in Computer Science, pages 3-17. Springer, 2015. [ bibtex | abstract | DOI | PDF | http ]
[5] Elvira Albert, Jesús Correas, Einar Broch Johnsen, and Guillermo Román-Dí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 275-292. Springer, 2015. [ bibtex | abstract | DOI | PDF | http ]

[6] Elvira Albert, Jesús Correas, and Guillermo Román-Díez. Non-Cumulative 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 85-100. Springer, 2015. [ bibtex | abstract | DOI | PDF | http ]

[7] Elvira Albert, Jesús Correas, Enrique Martín-Martín, and Guillermo Román-Dí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 104-119. Springer, 2014. [ bibtex | abstract | DOI | PDF | http ]

[8] Elvira Albert, Jesús Correas, and Guillermo Román-Díez. Peak Cost Analysis of Distributed Systems. In Markus Müller-Olm and Helmut Seidl, editors, Static Analysis - 21st International Symposium, SAS 2014, Munich, Germany, September 11-13, 2014. Proceedings, volume 8723 of Lecture Notes in Computer Science, pages 18-33. Springer, 2014. [ bibtex | abstract | DOI | PDF | http ]

[9] Elvira Albert, Puri Arenas, Antonio Flores-Montoya, Samir Genaim, Miguel Gómez-Zamalloa, Enrique Martin-Martin, Germán Puebla, and Guillermo Román-Dí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 562-567. Springer, 2014. [ bibtex | abstract | DOI | PDF | http ]

[10] Elvira Albert, Jesús Correas, Germán Puebla, and Guillermo Román-Dí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 285-300. Springer, June 2013. [ bibtex | abstract | DOI | PDF | http ]

[11] Elvira Albert, Richard Bubel, Samir Genaim, Reiner Hähnle, and Guillermo Román-Dí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 130-145. Springer, March 2012. [ bibtex | abstract | DOI | PDF | http ]

[12] Elvira Albert, Jesús Correas, Germán Puebla, and Guillermo Román-Dí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 23-24, 2012, pages 25-34. ACM Press, January 2012. [ bibtex | abstract | DOI | PDF | http ]

[13] Elvira Albert, Jesús Correas, Germán Puebla, and Guillermo Román-Dí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án-Díez. Verified Resource Guarantees using COSTA and KeY. In Siau-Cheng 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 24-25, 2011, SIGPLAN, pages 73-76. ACM, 2011. [ bibtex | abstract | DOI | DOI | PDF ]

[15] Elvira Albert, Puri Arenas, Samir Genaim, Miguel Gómez-Zamalloa, Germán Puebla, Diana Ramirez, Guillermo Román-Dí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 109-121. Elsevier, September 2009. [ bibtex | abstract | DOI | PDF ]

Publication in Workshops

[1] Elvira Albert, Samir Genaim, and Guillermo Román-Dí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án-Dí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án-Dí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 33-46. Springer, 2016. [ bibtex | abstract | DOI | http ]
[2] Elvira Albert, Diego Esteban Alonso Blas, Puri Arenas, Jesús Correas, Antonio Flores-Montoya, Samir Genaim, Miguel Gómez-Zamalloa, Abu Naser Masud, Germán Puebla, José Miguel Rojas, Guillermo Román-Dí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 24-28, 2012, Revised Lectures, volume 7866 of Lecture Notes in Computer Science, pages 119-144. Springer, 2013. [ bibtex | abstract | DOI | PDF | http ]