Document Open Access Logo

Towards Property-Based Testing of Smart Contracts Using Gas Analysis (Short Paper)

Authors Elvira Albert , Emanuele De Angelis , Marco Di Ianni , Fabio Fioravanti , Pablo Gordillo

PDF

File

Thumbnail PDF
PDF
OASIcs.FMBC.2026.9.pdf
  • Filesize: 0.58 MB
  • 8 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic and verification
  • Software and its engineering → Formal methods
  • Software and its engineering → Software testing and debugging
Keywords
  • Property-based Testing
  • Blockchain
  • Ethereum
  • Gas

Metrics

Abstract

Testing has become an integral part of the software development process in order to ensure the correct and safe execution of programs. A powerful approach to testing is property-based testing that aims at generating unit tests that verify that a certain property of interest holds. However, smart contracts are also characterized by important non-functional aspects, such as the gas consumption required to execute their functions. Static gas analyzers are able to obtain parametric gas bounds - that soundly over-approximate - the gas consumption of executing each of the public functions within a smart contract. This paper discusses our ideas towards combining both formal methods, property-based testing and gas analysis, in order to generate gas-aware unit tests that can ensure the gas requirements provided by the programmers.

Cite As Get BibTex

Elvira Albert, Emanuele De Angelis, Marco Di Ianni, Fabio Fioravanti, and Pablo Gordillo. Towards Property-Based Testing of Smart Contracts Using Gas Analysis (Short Paper). In 7th International Workshop on Formal Methods for Blockchains (FMBC 2026). Open Access Series in Informatics (OASIcs), Volume 142, pp. 9:1-9:8, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026) https://doi.org/10.4230/OASIcs.FMBC.2026.9

Author Details

Elvira Albert
  • Complutense University of Madrid, Spain
Emanuele De Angelis
  • IASI-CNR, Rome, Italy
Marco Di Ianni
  • DEc, University G. d'Annunzio, Chieti-Pescara, Italy
Fabio Fioravanti
  • DEc, University G. d'Annunzio, Chieti-Pescara, Italy
Pablo Gordillo
  • Complutense University of Madrid, Spain

Funding

This work was funded partially by the Spanish MCI, Comunidad de Madrid, AEI and FEDER (EU) projects PID2021-122830OB-C41, PID2024-157044OB-C31 and TEC-2024/COM-235, the BOVIR project PR17/24-31926 (Line A: early-career researchers, an action funded by the Community of Madrid within the framework of the 6th PRICIT 2022-2025 signed between the CAM and the UCM).

Acknowledgements

Emanuele De Angelis and Fabio Fioravanti are members of the INdAM-GNCS research group.

References

  1. Ethereum JSON-RPC Specification for eth_estimateGas. https://ethereum.github.io/execution-apis/api/methods/eth_estimateGas/, 2025.
  2. EVM Codes: An Ethereum Virtual Machine Opcodes Interactive Reference. https://www.evm.codes/, 2025.
  3. Foundry. https://getfoundry.sh/, 2025.
  4. Elvira Albert, Puri Arenas, Samir Genaim, and Germán Puebla. Automatic inference of upper bounds for recurrence relations in cost analysis. In María Alpuente and Germán Vidal, editors, Static Analysis, 15th International Symposium, SAS 2008, Valencia, Spain, July 16-18, 2008. Proceedings, volume 5079 of LNCS, pages 221-237. Springer, 2008. URL: https://doi.org/10.1007/978-3-540-69166-2_15.
  5. 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. J. Syst. Softw., 176:110923, 2021. URL: https://doi.org/10.1016/J.JSS.2021.110923.
  6. Morena Barboni, Andrea Morichetta, and Andrea Polini. Sumo: A mutation testing approach and tool for the ethereum blockchain. Journal of Systems and Software, 193:111445, 2022. URL: https://doi.org/10.1016/j.jss.2022.111445.
  7. Zhuo Cai, Soroush Farokhnia, Amir Kafshdar Goharshady, and S. Hitarth. Asparagus: Automated synthesis of parametric gas upper-bounds for smart contracts. Proc. ACM Program. Lang., 7(OOPSLA2):882-911, 2023. URL: https://doi.org/10.1145/3622829.
  8. Patrick Chapman, Dianxiang Xu, Lin Deng, and Yin Xiong. Deviant: A mutation testing tool for solidity smart contracts. In 2019 IEEE International Conference on Blockchain (Blockchain), pages 319-324, 2019. URL: https://doi.org/10.1109/Blockchain.2019.00050.
  9. Zilin Chen, Christine Rizkallah, Liam O'Connor, Partha Susarla, Gerwin Klein, Gernot Heiser, and Gabriele Keller. Property-based testing: Climbing the stairway to verification. In Bernd Fischer, Lola Burgueño, and Walter Cazzola, editors, Proceedings of the 15th ACM SIGPLAN International Conference on Software Language Engineering, SLE 2022, Auckland, New Zealand, December 6-7, 2022, pages 84-97. ACM, 2022. URL: https://doi.org/10.1145/3567512.3567520.
  10. Koen Claessen and John Hughes. Quickcheck: a lightweight tool for random testing of haskell programs. In Martin Odersky and Philip Wadler, editors, Proceedings of the Fifth ACM SIGPLAN International Conference on Functional Programming (ICFP '00), Montreal, Canada, September 18-21, 2000, pages 268-279. ACM, 2000. URL: https://doi.org/10.1145/351240.351266.
  11. S.W. Driessen, D. Di Nucci, D.A. Tamburri, and W.J. van den Heuvel. SolAR: Automated test-suite generation for solidity smart contracts. Science of Computer Programming, 232:103036, 2024. URL: https://doi.org/10.1016/j.scico.2023.103036.
  12. George Fink and Karl Levitt. Property-based testing of privileged programs. In In Tenth Annual Computer Security Applications Conference. IEEE Computer Society Press, pages 154-163, 1994. URL: https://doi.org/10.1109/CSAC.1994.367311.
  13. Harrison Goldstein, Joseph W. Cutler, Daniel Dickstein, Benjamin C. Pierce, and Andrew Head. Property-based testing in practice. Proceedings - International Conference on Software Engineering, pages 2307-2319, May 2024. URL: https://doi.org/10.1145/3597503.3639581.
  14. Gustavo Grieco, Will Song, Artur Cygan, Josselin Feist, and Alex Groce. Echidna: effective, usable, and fast fuzzing for smart contracts. In Proceedings of the 29th ACM SIGSOFT International Symposium on Software Testing and Analysis, ISSTA 2020, pages 557-560, New York, NY, USA, 2020. Association for Computing Machinery. URL: https://doi.org/10.1145/3395363.3404366.
  15. Dick Hamlet. Functional vs. non-functional properties. Composing Software Components, pages 311-318, 2010. URL: https://doi.org/10.1007/978-1-4419-7148-7_20.
  16. Bo Jiang, Ye Liu, and W. K. Chan. ContractFuzzer: fuzzing smart contracts for vulnerability detection. In Marianne Huchard, Christian Kästner, and Gordon Fraser, editors, Proceedings of the 33rd ACM/IEEE International Conference on Automated Software Engineering, ASE 2018, Montpellier, France, September 3-7, 2018, pages 259-269. ACM, 2018. URL: https://doi.org/10.1145/3238147.3238177.
  17. Mikkel Milo, Eske Hoy Nielsen, Danil Annenkov, and Bas Spitters. Finding smart contract vulnerabilities with concert’s property-based testing framework. In Zaynah Dargaye and Clara Schneidewind, editors, 4th International Workshop on Formal Methods for Blockchains, FMBC@CAV 2022, Haifa, Israel, August 11, 2022, volume 105 of OASIcs, pages 2:1-2:13. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022. URL: https://doi.org/10.4230/OASIcs.FMBC.2022.2.
  18. Bernhard Mueller. Smashing Ethereum Smart Contracts for Fun and Real Profit.(2018). In The 9th annual HITB Security Conference, 2018. Google Scholar
  19. Zoe Paraskevopoulou, Catalin Hritcu, Maxime Dénès, Leonidas Lampropoulos, and Benjamin C. Pierce. Foundational property-based testing. In Christian Urban and Xingyuan Zhang, editors, Interactive Theorem Proving - 6th International Conference, ITP 2015, Nanjing, China, August 24-27, 2015, Proceedings, volume 9236 of Lecture Notes in Computer Science, pages 325-343. Springer, 2015. URL: https://doi.org/10.1007/978-3-319-22102-1_22.
  20. Manuel J. C. S. Reis. Property-based testing for cybersecurity: Towards automated validation of security protocols. Computers 2025, Vol. 14,, 14, May 2025. URL: https://doi.org/10.3390/COMPUTERS14050179.
  21. Célio Gil Gouveia Rodrigues. Property-based testing of erc-20 smart contracts. Master’s thesis, Universidade do Porto (Portugal), 2020. Google Scholar
  22. Roberto Sebastiani and Patrick Trentin. Optimathsat: A tool for optimization modulo theories. Journal of Automated Reasoning, 64(3):423-460, 2020. URL: https://doi.org/10.1007/S10817-018-09508-6.
  23. Lars Stegeman. Solitor: runtime verification of smart contracts on the ethereum network. Master’s thesis, University of Twente, 2018. Google Scholar
  24. Gavin Wood et al. Ethereum: A secure decentralised generalised transaction ledger. Ethereum project yellow paper, (2025):1-42, 2025. Google Scholar
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2026 Schloss Dagstuhl – LZI GmbH Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact