ABSTRACT Property Inference from Program Executions ∗

Software verification techniques require properties that define the intended behavior of a system be specified. Generating such properties is often very difficult and serves as an impediment to the adoption of verification techniques. Techniques that leverage program executions to infer these properties are a promising avenue for automatically generating these properties. In this paper, we propose a property inference approach that leverages event traces derived from program executions to efficiently infer properties that are subtle variations of commonly occurring properties. We define inference templates that represent sets of these properties and describe our inference algorithm that refines these templates based on event traces. 1