| Software is difficult to write and maintain. Much of the challenge in developing a program lies in specifying it---understanding precisely what it should be doing. Both human-oriented tasks (like fixing a bug) and automated tasks (like mechanical verification) require knowledge of a program's intended behavior. For the vast majority of software projects, though, complete and well-documented specifications simply do not exist. Writing specifications---discovering and codifying intent---is a time-consuming and largely manual process.;This dissertation presents research into easing this process through automation. The work has focused on the problem of automatically "inferring" specifications directly from programs by analyzing their behavior. This dissertation presents a family of related algorithms, frameworks, and tools for reverse engineering a specific (but common) class of specification: temporal safety properties. It also includes a presentation of OCD, a software tool that leverages these "inference" techniques to both learn specifications and find bugs---simultaneously and fully automatically. Each presented algorithm and tool is practical, finding useful specifications and previously unknown bugs in large, widely-used software projects like Eclipse.;This dissertation concludes with a discussion of future work on this topic, including an outline of my vision of a new research area I am calling Intelligent Program Analysis. |
