Javert: fully automatic mining of general temporal properties from dynamic traces

Program specifications are important for many tasks during software design, development, and maintenance. Among these, temporal specifications are particularly useful. They express formal correctness requirements of an application's ordering of specific actions and events during execution, such as the strict alternation of acquisition and release of locks. Despite their importance, temporal specifications are often missing, incomplete, or described only informally. Many techniques have been proposed that mine such specifications from execution traces or program source code. However, existing techniques mine only simple patterns, or they mine a single complex pattern that is restricted to a particular set of manually selected events. There is no practical, automatic technique that can mine general temporal properties from execution traces. In this paper, we present Javert, the first general specification mining framework that can learn, fully automatically, complex temporal proper...

• Type: Conference
• Year: 2008
• Where: SIGSOFT
• Authors: Mark Gabel, Zhendong Su
• Keywords: Complex Temporal Properties, Execution Traces, SIGSOFT 2008, Software Engineering, Temporal Specifications