CAREER: Automatically Generating Specifications to Improve Program Correctness and Maintainability

Massachusetts Institute Of Technology, Cambridge MA

Investigators

Abstract

CCR-0133580 CAREER: Automatically Generating Specifications to Improve Program Correctness and Maintainability Michael D. Ernst Ensuring software correctness, modifying software, and many other software engineering tasks are greatly eased by the presence of specifications that document program behavior. Unfortunately, specifications are usually absent, leading to problems with program understanding and maintenance. This research extends work in automatically generating (inferring) partial program specifications from program executions. The research goals are to detect conditional invariants (implications) that are true only sometimes, to scale the technology, to enable online processing, to investigate new inference strategies, to improve usability, to evaluate via experiments and case studies, to integrate the techniques and tools into education, and to transfer technology to industry. The research has three broad impacts: (1) it explains, advances, and evaluates the theory and practice of automatic generation of program specifications; (2) it enables easier, more effective, and broader use of specifications, by automating generation of partial specifications and by extending their scope to likely (as opposed to guaranteed) properties; and (3) it applies specifications to specific program tasks via new techniques and tools for program modification, testing, reuse, and documentation. Evaluation includes theoretical evaluations of the accuracy of the underlying techniques, case studies of substantial software projects, and controlled experiments to determine the efficacy of the resulting tools.