Dynamically Inferring Temporal Properties

Jinlin Yang and David Evans
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