Dynamically Inferring Temporal Properties

Jinlin Yang and David Evans

ACM SIGPLAN-SIGSOFT Workshop on Program Analysis for Software Tools and Engineering (PASTE 2004).
June 7-8, 2004, Washington DC, USA.

Abstract

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.

Download the whole paper [PDF, PS], my oral presentation at the workshop [PPT].