Dynamically inferring temporal properties

12 years 5 months ago
Dynamically inferring temporal properties
Model checking requires a specification of the target system’s desirable properties, some of which are temporal. Formulating a 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. Categories and Subject Descriptors D.2.4 [Software/Program Verification] General Terms Experimentation, Verification. Keywords Invariants, temporal properties, concurrent programming, dynamic analysis, property patterns.
Jinlin Yang, David Evans
Added 30 Jun 2010
Updated 30 Jun 2010
Type Conference
Year 2004
Authors Jinlin Yang, David Evans
Comments (0)