SolTG: A CHC-based Solidity Test Case Generator

TitleSolTG: A CHC-based Solidity Test Case Generator
Publication TypeConference Paper
Year of Publication2024
AuthorsBritikov, Konstantin, Zlatkin Ilia, Fedyukovich Grigory, Alt Leonardo, and Sharygina Natasha
Conference NameComputer Aided Verification
Abstract

Test coverage is an important metric for the development of blockchain smart contracts. In this paper, we present SolTG, an automated CHC-based test case generator for Solidity smart contracts. SolTG exhaustively enumerates symbolic formulas and makes calls to SMT solver to find input values under which the contract exhibits the corresponding behavior. Test cases synthesized by SolTG have the form of a sequence of function calls over concrete values of input parameters, which lead to a specific execution scenario. The tool supports multiple Solidity-specific features and is capable of generating high coverage for industrial-grade Solidity code. We present a detailed architecture of SolTG and the translation of smart contracts into their CHC representation that the tool relies on. We also present the experimental results for test generation on the regression and industrial benchmarks.