CAREER: Automatically Generating Specifications to Improve Program Correctness and Maintainability

点击翻译按钮获取中文摘要

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.