CAREER: Automatically Generating Specifications to Improve Program Correctness and Maintainability

职业：自动生成规范，以提高程序的正确性和可维护性确保软件的正确性，修改软件，和许多其他的软件工程任务大大减轻了规范的存在，文件程序的行为。不幸的是，通常缺乏规范，导致程序理解和维护方面的问题。这项研究扩展了从程序执行中自动生成（推断）部分程序规范的工作。研究目标是检测仅在某些时候才成立的条件不变量（含义），扩展技术，使在线处理成为可能，调查新的决策策略，提高可用性，通过实验和案例研究进行评估，将技术和工具整合到教育中，并将技术转移到工业中。该研究具有三个广泛的影响：(1)它解释、推进和评估了程序规范自动生成的理论和实践；(2)通过自动生成部分规范并将其范围扩展到可能（而不是保证）的属性，它使规范更容易、更有效和更广泛地使用；(3)它通过新的技术和工具将规范应用于特定的程序任务，用于程序修改、测试、重用和文档。评估包括对基础技术准确性的理论评估，对实质性软件项目的案例研究，以及确定最终工具有效性的控制实验。

CCR-0133580CAREER: Automatically Generating Specifications to Improve Program Correctness and MaintainabilityMichael D. ErnstEnsuring software correctness, modifying software, and many other softwareengineering tasks are greatly eased by the presence of specifications thatdocument program behavior. Unfortunately, specifications are usuallyabsent, leading to problems with program understanding and maintenance.This research extends work in automatically generating (inferring) partialprogram specifications from program executions. The research goals are todetect conditional invariants (implications) that are true only sometimes,to scale the technology, to enable online processing, to investigate newinference strategies, to improve usability, to evaluate via experiments andcase studies, to integrate the techniques and tools into education, and totransfer technology to industry. The research has three broad impacts: (1)it explains, advances, and evaluates the theory and practice of automaticgeneration of program specifications; (2) it enables easier, moreeffective, and broader use of specifications, by automating generation ofpartial specifications and by extending their scope to likely (as opposedto guaranteed) properties; and (3) it applies specifications to specificprogram tasks via new techniques and tools for program modification,testing, reuse, and documentation. Evaluation includes theoreticalevaluations of the accuracy of the underlying techniques, case studies ofsubstantial software projects, and controlled experiments to determine theefficacy of the resulting tools.