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.