Abstract Achieving high test coverage is important when developing blockchain smart contracts, but it could be challenging without automated reasoning tools. In this paper, we present SolTG, an automated test case generator for Solidity based on constrained Horn clauses (CHC). SolTG exhaustively enumerates symbolic path constraints from the contract’s CHC representation and makes calls to the Satisfiability Modulo Theories (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 exhibiting a high coverage for industrial-grade Solidity code. We present a detailed architecture of SolTG based on the existing translation of smart contracts into a CHC representation. We also present the experimental results for test generation on the regression and industrial benchmarks.

No abstract available.

Abstract State-of-the-art solvers for constrained Horn clauses (CHC) are successfully used to generate reachability facts from symbolic encodings of programs. In this paper, we present a new application to test-case generation: if a block of code is provably unreachable, no test case can be generated allowing to explore other blocks of code. Our new approach uses CHC to incrementally construct different program unrollings and extract test cases from models of satisfiable formulas. At the same time, a CHC solver keeps track of CHCs that represent unreachable blocks of code which makes the unrolling process more efficient. In practice, this lets our approach to terminate early while guaranteeing maximal coverage. Our implementation called Horntinuum exhibits promising performance: it generates high coverage in the majority of cases and spends less time on average than state-of-the-art.