SHF: Small: Automated Verification and Synthesis of Input Generators in Property-Based Testing Frameworks

Testing is one of the most popular and effective ways to discover bugs in software, so that they can be fixed before a system is deployed. In recent years, automated testing has emerged as an important strategy for identifying software defects. Under this paradigm, developers specify the environment in which they expect their program to execute, and the behaviors it should exhibit in that environment. Given these constraints, automated testing frameworks attempt to systematically explore a program's behaviors by executing it in randomly generated environments consistent with the developer's characterization. Any unexpected behaviors are then reported back to the developer, so that they can diagnose and repair the underlying problem. Property-based testing is a popular automated testing approach that relies on handwritten programs, called generators, to construct the environment under which a target system is tested. Since they are also programs, generators may themselves have bugs which hamper the efficacy of automated testing. On the one hand, a generator may be unsound, constructing spurious environments that are inconsistent with the developer's requirements. An unsound generator results in a poor utilization of resources, as time is wasted looking for valid inputs. On the other hand, a generator may be incomplete, failing to produce valid environments. An incomplete generator lowers the level of assurance provided by the testing framework, as potentially faulty behaviors may be unexplored. Typically, developers rely on manual inspection and postmortem analysis of test runs to assess the soundness and completeness of a generator; not surprisingly, these approaches are error-prone and difficult to scale with generator complexity. The goal of this project is to develop new techniques that enable precise reasoning about the soundness and completeness of generators. The project's novelties are the development of new specification and reasoning frameworks, expressive type systems, and synthesis algorithms, specialized for the construction and validation of generators in property-based testing frameworks. Taken together, the project's impacts are a pathway to meaningfully strengthen the assurance provided by property based testing frameworks, resulting in an overall improvement in the quality of software validated using property-based testing. The project is comprised of three main thrusts. The first thrust considers specification frameworks and representations for characterizing the space of inputs produced by generators that are relevant to the systems under test. New specification formalisms capable of describing completeness properties, specifications that capture effectful properties, and quantitative specifications that describe the distributions and biases used to generate candidate inputs, will be developed in this thrust. The second thrust explores techniques for automatically verifying the correctness of user-defined generators. These approaches will focus on type-based verification techniques and will be influenced by the form and expressivity of the logical specifications developed in the first thrust. Finally, the third technical thrust investigates the complementary problem of directly synthesizing generators from the specifications developed in the first thrust, providing a correct-by-construction pathway for developers to automatically obtain high-quality generators. This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.