Dr. Grigory Fedyukovich, an Assistant Professor in the Computer Science Department, and his Formal Methods research lab have published their recent work in the prestigious 36th International Conference on Computer Aided Verification (CAV 2024). CAV is recognized as a top-tier conference dedicated to the advancement of the theory and practice of computer-aided formal analysis methods for hardware and software systems. The research paper, titled “SolTG: A CHC-based Solidity Test Case Generator”, was also co-authored by Ilia Zlatkin, a recent CS MS graduate and the collaborators of Dr. Fedyukovich from the Ethereum Foundation and University of Lugano, Switzerland.
Modern approaches to automated reasoning about software, such as verification, synthesis, repair, and test case generation, follow a paradigm of delegating complex symbolic reasoning to automated theorem provers and logic solvers. Intermediate languages, such as the ones based on constrained Horn clauses (CHC), bridge the gap between the semantics of software and the chosen logic theories. In the paper, Dr. Fedyukovich and others present an automated test case generation approach for Solidity smart contracts based on their CHC representation. Test cases have the form of a sequence of function calls over concrete values of input parameters, under which the contract exhibits a particular execution. These values are generated by an underlying Satisfiability Modulo Theories (SMT) solver that receives a logic encoding of the contract execution and determines its feasibility via a satisfiability check. The approach aims to maximize the number of contract functions, branches, and lines that are collectively visited by a set of synthesized test cases.
The paper will be presented at the upcoming CAV 2024 conference in Montreal, Canada in July and will be published by Springer in the proceedings of the conference.