International Journals

[1] Elvira Albert, Pablo Gordillo, Alejandro Hernández-Cerezo, Albert Rubio, and Maria A. Schett. Super-Optimization of Smart Contracts. ACM Transactions on Software Engineering and Methodology, 31 Issue 4(70):1-29, 2022. [ bibtex | abstract | DOI | http ]

[2] 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 ]

[3] Jesús Correas, Pablo Gordillo, and Guillermo Román-Díez. Static Profiling and Optimization of Ethereum Smart Contracts Using Resource Analysis. IEEE Access, 9:25495-25507, 2021. [ bibtex | abstract | DOI | PDF ]

International Conferences

[1] Elvira Albert, Pablo Gordillo, Alejandro Hernández-Cerezo, Clara Rodríguez-Núñez, and Albert Rubio. Using Automated Reasoning Techniques for Enhancing the Efficiency and Security of (Ethereum) Smart Contracts. In Jasmin Blanchette, Laura Kovács, and Dirk Pattinson, editors, Automated Reasoning - 11th International Joint Conference, IJCAR 2022, Haifa, Israel, August 8-10, 2022, Proceedings, volume 13385 of Lecture Notes in Computer Science, pages 3-7. Springer, 2022. [ bibtex | abstract | DOI | PDF ]
[2] Elvira Albert, Pablo Gordillo, Alejandro Hernández-Cerezo, and Albert Rubio. A Max-SMT Superoptimizer for EVM handling Memory and Storage. In Dana Fisman and Grigore Rosu, editors, 28th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2022. Proceedings, volume 13243 of Lecture Notes in Computer Science, pages 201-219. Springer, 2022. [ bibtex | abstract | DOI | PDF ]

[3] Elvira Albert, Pablo Gordillo, Albert Rubio, and Maria A. Schett. Synthesis of Super-Optimized Smart Contracts using Max-SMT. In 32nd International Conference on Computer Aided Verification, CAV 2020. Proceedings, volume 12224 of Lecture Notes in Computer Science, pages 177-200, 2020. [ bibtex | abstract | DOI | PDF ]

[4] 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 ]

[5] 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 ]
[6] Elvira Albert, Pablo Gordillo, Albert Rubio, and Ilya Sergey. Running on Fumes: Preventing Out-Of-Gas Vulnerabilities in Ethereum Smart Contracts using Static Resource Analysis. In Pierre Ganty and Mohamed Kaâniche, editors, 13th International Conference on Verification and Evaluation of Computer and Communication Systems, VECoS 2019. Proceedings, volume 11847 of Lecture Notes in Computer Science, pages 63-78. Springer, 2019. [ bibtex | abstract | DOI | PDF ]

[7] 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 ]

[8] Elvira Albert, Pablo Gordillo, Benjamin Livshits, Albert Rubio, and Ilya Sergey. EthIR: A Framework for High-Level Analysis of Ethereum Bytecode. In Shuvendu Lahiri and Chao Wang, editors, 16th International Symposium on Automated Technology for Verification and Analysis, ATVA 2018. Proceedings, volume 11138 of Lecture Notes in Computer Science, pages 513-520. Springer, 2018. [ bibtex | abstract | DOI | PDF ]

[9] Elvira Albert, Samir Genaim, and Pablo Gordillo. May-Happen-in-Parallel Analysis with Returned Futures. In Deepak D'Souza and K.Narayan Kumar, editors, 15th International Symposium on Automated Technology for Verification and Analysis, ATVA 2017. Proceedings, volume 10482 of Lecture Notes in Computer Science, pages 42-58. Springer, 2017. [ bibtex | abstract | DOI | PDF ]

[10] Elvira Albert, Samir Genaim, and Pablo Gordillo. May-Happen-in-Parallel Analysis for Asynchronous Programs with Inter-Procedural Synchronization. In Sandrine Blazy and Thomas P. Jensen, editors, Static Analysis - 22nd International Symposium, SAS 2015. Proceedings, volume 9291 of Lecture Notes in Computer Science, pages 72-89. Springer, 2015. [ bibtex | abstract | DOI | PDF | http ]

Technical Reports

[1] Elvira Albert, Jesús Correas, Pablo Gordillo, Alejandro Hernández-Cerezo, Guillermo Román-Díez, and Albert Rubio. Analyzing Smart Contracts: From EVM to a Sound Control-Flow Graph. Technical report, 2020. [ bibtex | abstract | PDF ]

Thesis

[1] Pablo Gordillo. Supervised by Elvira Albert and Samir Genaim. Static Analysis of Concurrent and Distributed Systems: Concurrent Objects and Ethereum Bytecode. PhD. Thesis, Facultad de Informática, Universidad Complutense de Madrid, January 2020. [ abstract | PDF | http ]

[2] Pablo Gordillo. Supervised by Elvira Albert and Samir Genaim. May-Happen-in-Parallel Analysis with Returned Futures. Master's Thesis, Facultad de Informática, Universidad Complutense de Madrid, July 2017. [ abstract | PDF | http ]

[3] Pablo Gordillo. Supervised by Elvira Albert and Samir Genaim. Static Analysis for Concurrent Objects: May-Happen-in-Parallel Analysis for Asynchronous Programs with Inter-Procedural Synchronization. Bachelor's Thesis, Facultad de Informática, Universidad Complutense de Madrid, June 2015. [ abstract | PDF | http ]

Quick Links

Recent News