Automatic Inference and Effective Application of Temporal Specifications

University Of Virginia Main Campus, Charlottesville VA

Investigators

Abstract

Abstract CCF-0541123 David Evans University of Virginia Title: CPA: Automatic Inference and Effective Use of Temporal Properties Understanding properties that constrain the ordering and occurrence of events is crucial for the dependability of complex software systems. Failures to satisfy needed properties can lead to deadlocks, data races, protocol violations, memory corruption, and incorrect results. There has been considerable progress in model checking and other program verification techniques which, along with improvements in available computing resources, has enabled checking temporal properties for large software systems. A substantial impediment to wider adoption and more effective use of these techniques, however, is the high degree of expertise and substantial effort required to identify important temporal properties and express them using a formal notation. This research seeks to develop techniques for automatically inferring important temporal properties and effectively using them to aid program verification, evolution, and other software development tasks. The project is developing and evaluating a dynamic analysis technique that infers properties from program traces and selects important properties using heuristics. The research will develop new theories and heuristics for measuring the importance of a temporal property that combine static and dynamic analysis techniques as well as producing methods for using inferred temporal properties to aid software development tasks.