CAREER: Automatically Generating Specifications to Improve Program Correctness and Maintainability

CCR-0133580 CAREER：自动生成规范以提高程序的正确性和可维护性Ernst确保软件的正确性，修改软件，和许多其他软件工程任务都大大简化了文档程序行为的规范的存在。 不幸的是，规范通常是缺席的，导致问题的程序理解和maintenance.This研究扩展工作自动生成（推断）partialprogram规格从程序执行。 研究的目标是检测条件不变量（含义），只有有时是真的，规模的技术，使在线处理，调查新的参考策略，提高可用性，通过实验和案例研究进行评估，将技术和工具整合到教育中，并将技术转移到工业中。 本文的研究有三个方面的影响：（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.