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

测试是发现软件中错误的最流行和最有效的方法之一，以便在部署系统之前修复错误。近年来，自动化测试已经成为识别软件缺陷的重要策略。在这种范式下，开发人员指定他们期望程序执行的环境，以及程序在该环境中应该表现出的行为。考虑到这些限制，自动化测试框架试图通过在与开发人员的特征一致的随机生成的环境中执行程序来系统地探索程序的行为。然后，任何意外的行为都会报告给开发人员，以便他们可以诊断和修复潜在的问题。基于属性的测试是一种流行的自动化测试方法，它依赖于手写程序（称为生成器）来构造测试目标系统的环境。由于它们也是程序，生成器本身可能有缺陷，这会妨碍自动化测试的效率。一方面，生成器可能是不可靠的，构造与开发人员的需求不一致的虚假环境。一个不健全的发电机会导致资源利用率低下，因为时间被浪费在寻找有效的输入。另一方面，生成器可能不完整，无法生成有效的环境。一个不完整的生成器降低了测试框架提供的保证水平，因为潜在的错误行为可能没有被发现。通常情况下，开发人员依靠手动检查和测试运行的事后分析来评估生成器的可靠性和完整性;毫不奇怪，这些方法容易出错，并且难以随生成器的复杂性而扩展。这个项目的目标是开发新的技术，使发电机的健全性和完整性的精确推理。该项目的新颖之处是开发新的规范和推理框架，表达类型系统和合成算法，专门用于基于属性的测试框架中的生成器的构建和验证。总的来说，该项目的影响是一条有意义地加强基于属性的测试框架提供的保证的途径，从而全面提高使用基于属性的测试验证的软件质量。 第一个推力考虑规范框架和表征的空间的输入产生的发电机，相关的测试中的系统。新的规格形式主义能够描述完整性的属性，规格，捕获有效的属性，和定量规格，描述用于生成候选输入的分布和偏差，将在这方面的努力。 第二个推力探索自动验证用户定义的生成器的正确性的技术。这些方法将侧重于基于类型的验证技术，并将受到第一次推力中开发的逻辑规范的形式和表达能力的影响。最后，第三个技术重点研究了从第一个重点开发的规范直接合成发电机的补充问题，为开发人员自动获得高质量发电机提供了一个正确的建设途径。该奖项反映了NSF的法定使命，并通过使用基金会的智力价值和更广泛的影响审查标准进行评估，被认为值得支持。

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.