Dynamically Inferring Temporal Properties
ACM SIGPLAN-SIGSOFT Workshop on Program Analysis for Software Tools and Engineering (PASTE 2004)
Washington, DC 7-8 June 2004
Model checking requires a specification of the target system's desirable properties, some of which are temporal. Formulating a temporal property of the system based on either its abstract model or implementation requires a deep understanding of its behavior and sophisticated knowledge of the chosen formalism. This has been a major impediment to documenting and verifying temporal properties. We propose a dynamic approach to automatically infer a program's temporal properties based on a set of property pattern templates. We describe a preliminary implementation of this approach, and report on our experience using it to discover interesting temporal properties of a small program.
Keywords: Invariants, temporal properties, concurrent programming, dynamic analysis, property patterns.
Complete Paper (6 pages)
[PDF]
Talk
Slides (Jinlin Yang)
Inexpensive Program Analysis Group Page
