Guillermo Román

Publications

2025

1. Harnessing heap analysis for the synthesis of superoptimized bytecode

   Albert, E., Correas, J., Gordillo, P., Román-Dı́ez Guillermo, & Rubio, A. (2025). Harnessing heap analysis for the synthesis of superoptimized bytecode. J. Syst. Softw., 221, 112284.
2. EasyRpl: A web-based tool for modelling and analysis of cross-organisational workflows

   Ali, M. R., Pun, V. K. I., & Román-Dı́ez Guillermo. (2025). EasyRpl: A web-based tool for modelling and analysis of cross-organisational workflows. CoRR, abs/2502.20972.

2024

1. Synthesis of Sound and Precise Storage Cost Bounds via Unsound Resource Analysis and Max-SMT

   Albert, E., Correas, J., Gordillo, P., Román-Dı́ez Guillermo, & Rubio, A. (2024). Synthesis of Sound and Precise Storage Cost Bounds via Unsound Resource Analysis and Max-SMT. In M. Christakis & M. Pradel (Eds.), Proceedings of the 33rd ACM SIGSOFT International Symposium on Software Testing and Analysis, ISSTA 2024, Vienna, Austria, September 16-20, 2024 (pp. 1186–1197). ACM.

2023

1. Inferring Needless Write Memory Accesses on Ethereum Bytecode

   Albert, E., Correas, J., Gordillo, P., Román-Dı́ez Guillermo, & Rubio, A. (2023). Inferring Needless Write Memory Accesses on Ethereum Bytecode. In S. Sankaranarayanan & N. Sharygina (Eds.), Tools and Algorithms for the Construction and Analysis of Systems - 29th International Conference, TACAS 2023, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Paris, France, April 22-27, 2023, Proceedings, Part I (Vol. 13993, pp. 448–466). Springer.
2. Inferring Needless Write Memory Accesses on Ethereum Bytecode (Extended Version)

   Albert, E., Correas, J., Gordillo, P., Román-Dı́ez Guillermo, & Rubio, A. (2023). Inferring Needless Write Memory Accesses on Ethereum Bytecode (Extended Version). CoRR, abs/2301.04757.
3. Artifact for paper "Harnessing Heap Analysis for the Synthesis of Superoptimized Bytecode" (Version 1)

   Albert, E., Correas, J., Gordillo, P., Román-Dı́ez Guillermo, & Rubio, A. (2023). Artifact for paper "Harnessing Heap Analysis for the Synthesis of Superoptimized Bytecode" (Version 1). Zenodo.
4. Artifact for paper "Harnessing Heap Analysis for the Synthesis of Superoptimized Bytecode" (Version 2)

   Albert, E., Correas, J., Gordillo, P., Román-Dı́ez Guillermo, & Rubio, A. (2023). Artifact for paper "Harnessing Heap Analysis for the Synthesis of Superoptimized Bytecode" (Version 2). Zenodo.
5. Artifact for paper "Harnessing Heap Analysis for the Synthesis of Superoptimized Bytecode" (Version 3)

   Albert, E., Correas, J., Gordillo, P., Román-Dı́ez Guillermo, & Rubio, A. (2023). Artifact for paper "Harnessing Heap Analysis for the Synthesis of Superoptimized Bytecode" (Version 3). Zenodo.
6. Artifact for paper "Harnessing Heap Analysis for the Synthesis of Superoptimized Bytecode" (Version 4)

   Albert, E., Correas, J., Gordillo, P., Román-Dı́ez Guillermo, & Rubio, A. (2023). Artifact for paper "Harnessing Heap Analysis for the Synthesis of Superoptimized Bytecode" (Version 4). Zenodo.
7. Artifact for paper "Harnessing Heap Analysis for the Synthesis of Superoptimized Bytecode" (Version 5)

   Albert, E., Correas, J., Gordillo, P., Román-Dı́ez Guillermo, & Rubio, A. (2023). Artifact for paper "Harnessing Heap Analysis for the Synthesis of Superoptimized Bytecode" (Version 5). Zenodo.
8. Artifact for paper "Harnessing Heap Analysis for the Synthesis of Superoptimized Bytecode" (Version 6)

   Albert, E., Correas, J., Gordillo, P., Román-Dı́ez Guillermo, & Rubio, A. (2023). Artifact for paper "Harnessing Heap Analysis for the Synthesis of Superoptimized Bytecode" (Version 6). Zenodo.
9. Artifact for paper "Harnessing Heap Analysis for the Synthesis of Superoptimized Bytecode" (Version 7)

   Albert, E., Correas, J., Gordillo, P., Román-Dı́ez Guillermo, & Rubio, A. (2023). Artifact for paper "Harnessing Heap Analysis for the Synthesis of Superoptimized Bytecode" (Version 7). Zenodo.

2022

1. When COSTA Met KeY: Verified Cost Bounds

   Albert, E., Genaim, S., Merayo, A., & Román-Dı́ez Guillermo. (2022). When COSTA Met KeY: Verified Cost Bounds. In W. Ahrendt, B. Beckert, R. Bubel, & E. B. Johnsen (Eds.), The Logic of Software. A Tasting Menu of Formal Methods - Essays Dedicated to Reiner Hähnle on the Occasion of His 60th Birthday (Vol. 13360, pp. 19–37). Springer.

2021

1. Static Profiling and Optimization of Ethereum Smart Contracts Using Resource Analysis

   Correas, J., Gordillo, P., & Román-Dı́ez Guillermo. (2021). Static Profiling and Optimization of Ethereum Smart Contracts Using Resource Analysis. IEEE Access, 9, 25495–25507.
2. Don’t run on fumes - Parametric gas bounds for smart contracts

   Albert, E., Correas, J., Gordillo, P., Román-Dı́ez Guillermo, & Rubio, A. (2021). Don’t run on fumes - Parametric gas bounds for smart contracts. J. Syst. Softw., 176, 110923.

2020

1. Smart, and also Reliable and Gas-Efficient, Contracts

   Albert, E., Correas, J., Gordillo, P., Román-Dı́ez Guillermo, & Rubio, A. (2020). Smart, and also Reliable and Gas-Efficient, Contracts. 13th IEEE International Conference on Software Testing, Validation and Verification, ICST 2020, Porto, Portugal, October 24-28, 2020, 2.
2. GASOL: Gas Analysis and Optimization for Ethereum Smart Contracts

   Albert, E., Correas, J., Gordillo, P., Román-Dı́ez Guillermo, & Rubio, A. (2020). GASOL: Gas Analysis and Optimization for Ethereum Smart Contracts. In A. Biere & D. Parker (Eds.), Tools and Algorithms for the Construction and Analysis of Systems - 26th International Conference, TACAS 2020, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Dublin, Ireland, April 25-30, 2020, Proceedings, Part II (Vol. 12079, pp. 118–125). Springer.
3. Analyzing Smart Contracts: From EVM to a sound Control-Flow Graph

   Albert, E., Correas, J., Gordillo, P., Román-Dı́ez Guillermo, & Rubio, A. (2020). Analyzing Smart Contracts: From EVM to a sound Control-Flow Graph. CoRR, abs/2004.14437.

2019

1. Time analysis of actor programs

   Laneve, C., Lienhardt, M., Pun, K. I., & Román-Dı́ez Guillermo. (2019). Time analysis of actor programs. J. Log. Algebraic Methods Program., 105, 1–27.
2. Peak resource analysis of concurrent distributed systems

   Albert, E., Correas, J., & Román-Dı́ez Guillermo. (2019). Peak resource analysis of concurrent distributed systems. J. Syst. Softw., 149, 35–62.
3. SAFEVM: a safety verifier for Ethereum smart contracts

   Albert, E., Correas, J., Gordillo, P., Román-Dı́ez Guillermo, & Rubio, A. (2019). SAFEVM: a safety verifier for Ethereum smart contracts. In D. Zhang & A. Møller (Eds.), Proceedings of the 28th ACM SIGSOFT International Symposium on Software Testing and Analysis, ISSTA 2019, Beijing, China, July 15-19, 2019 (pp. 386–389). ACM.
4. SAFEVM: A Safety Verifier for Ethereum Smart Contracts

   Albert, E., Correas, J., Gordillo, P., Román-Dı́ez Guillermo, & Rubio, A. (2019). SAFEVM: A Safety Verifier for Ethereum Smart Contracts. CoRR, abs/1906.04984.
5. GASOL: Gas Analysis and Optimization for Ethereum Smart Contracts

   Albert, E., Correas, J., Gordillo, P., Román-Dı́ez Guillermo, & Rubio, A. (2019). GASOL: Gas Analysis and Optimization for Ethereum Smart Contracts. CoRR, abs/1912.11929.

2018

1. Parallel Cost Analysis

   Albert, E., Correas, J., Johnsen, E. B., Pun, V. K. I., & Román-Dı́ez Guillermo. (2018). Parallel Cost Analysis. ACM Trans. Comput. Log., 19(4), 31:1–31:37.

2017

1. SICOMORo-CM: Development of Trustworthy Systems via Models and Advanced Tools

   Albert, E., Cañizares, P. C., Guerra, E., de Lara, J., Marcos, E., Núñez, M., Román-Dı́ez Guillermo, Vara, J. M., & Zanardini, D. (2017). SICOMORo-CM: Development of Trustworthy Systems via Models and Advanced Tools. In M. Seidl & S. Zschaler (Eds.), Software Technologies: Applications and Foundations - STAF 2017 Collocated Workshops, Marburg, Germany, July 17-21, 2017, Revised Selected Papers (Vol. 10748, pp. 367–374). Springer.

2016

1. A formal verification framework for static analysis - As well as its instantiation to the resource analyzer COSTA and formal verification tool KeY

   Albert, E., Bubel, R., Genaim, S., Hähnle, R., Puebla, G., & Román-Dı́ez Guillermo. (2016). A formal verification framework for static analysis - As well as its instantiation to the resource analyzer COSTA and formal verification tool KeY. Softw. Syst. Model., 15(4), 987–1012.
2. Resource Analysis of Distributed Systems

   Albert, E., Correas, J., & Román-Dı́ez Guillermo. (2016). Resource Analysis of Distributed Systems. In E. Ábrahám, M. M. Bonsangue, & E. B. Johnsen (Eds.), Theory and Practice of Formal Methods - Essays Dedicated to Frank de Boer on the Occasion of His 60th Birthday (Vol. 9660, pp. 33–46). Springer.

2015

1. Quantified abstract configurations of distributed systems

   Albert, E., Fernández, J. C., Puebla, G., & Román-Dı́ez Guillermo. (2015). Quantified abstract configurations of distributed systems. Formal Aspects Comput., 27(4), 665–699.
2. Object-sensitive cost analysis for concurrent objects

   Albert, E., Arenas, P., Fernández, J. C., Genaim, S., Gómez-Zamalloa, M., Puebla, G., & Román-Dı́ez Guillermo. (2015). Object-sensitive cost analysis for concurrent objects. Softw. Test. Verification Reliab., 25(3), 218–271.
3. A multi-domain incremental analysis engine and its application to incremental resource analysis

   Albert, E., Fernández, J. C., Puebla, G., & Román-Dı́ez Guillermo. (2015). A multi-domain incremental analysis engine and its application to incremental resource analysis. Theor. Comput. Sci., 585, 91–114.
4. Resource Analysis: From Sequential to Concurrent and Distributed Programs

   Albert, E., Arenas, P., Correas, J., Genaim, S., Gómez-Zamalloa, M., Martin-Martin, E., Puebla, G., & Román-Dı́ez Guillermo. (2015). Resource Analysis: From Sequential to Concurrent and Distributed Programs. In N. S. Bjørner & F. S. de Boer (Eds.), FM 2015: Formal Methods - 20th International Symposium, Oslo, Norway, June 24-26, 2015, Proceedings (Vol. 9109, pp. 3–17). Springer.
5. Parallel Cost Analysis of Distributed Systems

   Albert, E., Correas, J., Johnsen, E. B., & Román-Dı́ez Guillermo. (2015). Parallel Cost Analysis of Distributed Systems. In S. Blazy & T. P. Jensen (Eds.), Static Analysis - 22nd International Symposium, SAS 2015, Saint-Malo, France, September 9-11, 2015, Proceedings (Vol. 9291, pp. 275–292). Springer.
6. Non-cumulative Resource Analysis

   Albert, E., Fernández, J. C., & Román-Dı́ez Guillermo. (2015). Non-cumulative Resource Analysis. In C. Baier & C. Tinelli (Eds.), Tools and Algorithms for the Construction and Analysis of Systems - 21st International Conference, TACAS 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11-18, 2015. Proceedings (Vol. 9035, pp. 85–100). Springer.

2014

1. Conditional termination of loops over heap-allocated data

   Albert, E., Arenas, P., Genaim, S., Puebla, G., & Román-Dı́ez Guillermo. (2014). Conditional termination of loops over heap-allocated data. Sci. Comput. Program., 92, 2–24.
2. Static Inference of Transmission Data Sizes in Distributed Systems

   Albert, E., Fernández, J. C., Martin-Martin, E., & Román-Dı́ez Guillermo. (2014). Static Inference of Transmission Data Sizes in Distributed Systems. In T. Margaria & B. Steffen (Eds.), Leveraging Applications of Formal Methods, Verification and Validation. Specialized Techniques and Applications - 6th International Symposium, ISoLA 2014, Imperial, Corfu, Greece, October 8-11, 2014, Proceedings, Part II (Vol. 8803, pp. 104–119). Springer.
3. Peak Cost Analysis of Distributed Systems

   Albert, E., Fernández, J. C., & Román-Dı́ez Guillermo. (2014). Peak Cost Analysis of Distributed Systems. In M. Müller-Olm & H. Seidl (Eds.), Static Analysis - 21st International Symposium, SAS 2014, Munich, Germany, September 11-13, 2014. Proceedings (Vol. 8723, pp. 18–33). Springer.
4. SACO: Static Analyzer for Concurrent Objects

   Albert, E., Arenas, P., Flores-Montoya, A., Genaim, S., Gómez-Zamalloa, M., Martin-Martin, E., Puebla, G., & Román-Dı́ez Guillermo. (2014). SACO: Static Analyzer for Concurrent Objects. In E. Ábrahám & K. Havelund (Eds.), Tools and Algorithms for the Construction and Analysis of Systems - 20th International Conference, TACAS 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Grenoble, France, April 5-13, 2014. Proceedings (Vol. 8413, pp. 562–567). Springer.

2013

1. Quantified Abstractions of Distributed Systems

   Albert, E., Correas, J., Puebla, G., & Román-Dı́ez Guillermo. (2013). Quantified Abstractions of Distributed Systems. In E. B. Johnsen & L. Petre (Eds.), Integrated Formal Methods, 10th International Conference, IFM 2013, Turku, Finland, June 10-14, 2013. Proceedings (Vol. 7940, pp. 285–300). Springer.

2012

1. Advanced Topics in Resource Analysis: Certification, Incrementality, Concurrency and Array-Sensitivity

   Román-Dı́ez Guillermo. (2012). Advanced Topics in Resource Analysis: Certification, Incrementality, Concurrency and Array-Sensitivity [PhD thesis, Technical University of Madrid, Spain].
2. Verified Resource Guarantees for Heap Manipulating Programs

   Albert, E., Bubel, R., Genaim, S., Hähnle, R., & Román-Dı́ez Guillermo. (2012). Verified Resource Guarantees for Heap Manipulating Programs. In J. de Lara & A. Zisman (Eds.), Fundamental Approaches to Software Engineering - 15th International Conference, FASE 2012, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2012, Tallinn, Estonia, March 24 - April 1, 2012. Proceedings (Vol. 7212, pp. 130–145). Springer.
3. Automatic Inference of Bounds on Resource Consumption

   Albert, E., Alonso-Blas, D. E., Arenas, P., Correas, J., Flores-Montoya, A., Genaim, S., Gómez-Zamalloa, M., Masud, A. N., Puebla, G., Rojas, J. M., Román-Dı́ez Guillermo, & Zanardini, D. (2012). Automatic Inference of Bounds on Resource Consumption. In E. Giachino, R. Hähnle, F. S. de Boer, & M. M. Bonsangue (Eds.), Formal Methods for Components and Objects - 11th International Symposium, FMCO 2012, Bertinoro, Italy, September 24-28, 2012, Revised Lectures (Vol. 7866, pp. 119–144). Springer.
4. Incremental resource usage analysis

   Albert, E., Correas, J., Puebla, G., & Román-Dı́ez Guillermo. (2012). Incremental resource usage analysis. In O. Kiselyov & S. J. Thompson (Eds.), Proceedings of the ACM SIGPLAN 2012 Workshop on Partial Evaluation and Program Manipulation, PEPM 2012, Philadelphia, Pennsylvania, USA, January 23-24, 2012 (pp. 25–34). ACM.

2011

1. Verified resource guarantees using COSTA and KeY

   Albert, E., Bubel, R., Genaim, S., Hähnle, R., Puebla, G., & Román-Dı́ez Guillermo. (2011). Verified resource guarantees using COSTA and KeY. In S.-C. Khoo & J. G. Siek (Eds.), Proceedings of the 2011 ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation, PEPM 2011, Austin, TX, USA, January 24-25, 2011 (pp. 73–76). ACM.

2009

1. Termination and Cost Analysis with COSTA and its User Interfaces

   Albert, E., Arenas, P., Genaim, S., Gómez-Zamalloa, M., Puebla, G., Ramı́rez-Deantes Diana V., Román-Dı́ez Guillermo, & Zanardini, D. (2009). Termination and Cost Analysis with COSTA and its User Interfaces. In P. Lucio, G. Moreno, & R. Peña (Eds.), Proceedings of the Ninth Spanish Conference on Programming and Languages, PROLE 2009, San Sebastián, Spain, September 9-11, 2009 (Vol. 258, Number 1, pp. 109–121). Elsevier.