DROPS

Document

Short Paper

DOI: 10.4230/OASIcs.FMBC.2026.9

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

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

Published in: OASIcs, Volume 142, 7th International Workshop on Formal Methods for Blockchains (FMBC 2026)

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

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)

Copy BibTex To Clipboard

@InProceedings{albert_et_al:OASIcs.FMBC.2026.9,
  author =	{Albert, Elvira and De Angelis, Emanuele and Di Ianni, Marco and Fioravanti, Fabio and Gordillo, Pablo},
  title =	{{Towards Property-Based Testing of Smart Contracts Using Gas Analysis}},
  booktitle =	{7th International Workshop on Formal Methods for Blockchains (FMBC 2026)},
  pages =	{9:1--9:8},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-424-6},
  ISSN =	{2190-6807},
  year =	{2026},
  volume =	{142},
  editor =	{Bartoletti, Massimo and Marmsoler, Diego},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.FMBC.2026.9},
  URN =		{urn:nbn:de:0030-drops-257069},
  doi =		{10.4230/OASIcs.FMBC.2026.9},
  annote =	{Keywords: Property-based Testing, Blockchain, Ethereum, Gas}
}

Document

DOI: 10.4230/LIPIcs.ICLP.2012.98

Towards Testing Concurrent Objects in CLP

Authors: Elvira Albert, Puri Arenas, and Miguel Gómez-Zamalloa

Published in: LIPIcs, Volume 17, Technical Communications of the 28th International Conference on Logic Programming (ICLP'12) (2012)

Abstract

Testing is a vital part of the software development process. It is even more so in the context of concurrent languages, since due to undesired task interleavings and to unexpected behaviours of the underlying task scheduler, errors can go easily undetected. This paper studies the extension of the CLP-based framework for glass-box test data generation of sequential programs to the context of concurrent objects, a concurrency model which constitutes a promising solution to concurrency in OO languages. Our framework combines standard termination and coverage criteria used for testing sequential programs with specific criteria which control termination and coverage from the concurrency point of view, e.g., we can limit the number of task interleavings allowed and the number of loop unrollings performed in each parallel component, etc.

Cite as

Elvira Albert, Puri Arenas, and Miguel Gómez-Zamalloa. Towards Testing Concurrent Objects in CLP. In Technical Communications of the 28th International Conference on Logic Programming (ICLP'12). Leibniz International Proceedings in Informatics (LIPIcs), Volume 17, pp. 98-108, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)

Copy BibTex To Clipboard

@InProceedings{albert_et_al:LIPIcs.ICLP.2012.98,
  author =	{Albert, Elvira and Arenas, Puri and G\'{o}mez-Zamalloa, Miguel},
  title =	{{Towards Testing Concurrent Objects in CLP}},
  booktitle =	{Technical Communications of the 28th International Conference on Logic Programming (ICLP'12)},
  pages =	{98--108},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-43-9},
  ISSN =	{1868-8969},
  year =	{2012},
  volume =	{17},
  editor =	{Dovier, Agostino and Santos Costa, V{\'\i}tor},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICLP.2012.98},
  URN =		{urn:nbn:de:0030-drops-36134},
  doi =		{10.4230/LIPIcs.ICLP.2012.98},
  annote =	{Keywords: Testing, Glass-box Test Data Generation, Active Objects, Symbolic Execution}
}

Search Results

Documents authored by Albert, Elvira

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

Abstract

Cite as

Towards Testing Concurrent Objects in CLP

Abstract

Cite as

Thanks for your feedback!

Could not send message