(web page under construction!)
It's best if all programs and software projects are developed with clear, precise and documented specifications. However, due to hard deadlines and 'short-time-to-market' requirement, software products often come with poor, incomplete and even without any documented specifications. This situation is aggravated by a phenomenon termed as software evolution. As software evolves the documented specification is often not updated. This might render the original documented specification of little use after several cycles of program evolution.
In our research, we investigate various means to discover software specifications from its associated program execution traces. One of the novel techniques we have proposed is to mine from program execution traces a sound and complete set of statistically significant temporal rules. The extracted temporal rules act as specifications of the associated software, as they reveal invariants that the program observes, and will consequently guide developers to understand the program behaviors, and facilitate all downstream applications such as verification and debugging. A salient feature of this technique is the ability to discover temporal rules of arbitrary lengths, while ensuring scalability and utility of our approach.
We have also investigated and proposed other techniques of specification mining, and applied the discovered specification to enhance the productivity of programmers.