Title: Fully Automatic Mining of General Temporal Properties 

Presenter: Prof. Zhendong Su Department of Computer Science University of California, Davis, USA 

Time: 10:00-12:00, July 14th, 2009 (Tuesday) 

Location: Room 504, Building MengMinwei

Program specifications are important in many phases of the software development process, but they are often omitted or incomplete. An important class of specifications takes the form of temporal properties that prescribe proper usage of components of a software system. Recent work has focused on the automated inference of temporal specifications from the static or runtime behavior of programs. However, existing techniques mine only simple patterns or a single complex pattern restricted to some manually selected events. There is no practical, automatic technique that can mine general temporal properties. This talk will present Javert, the first general specification mining framework that can learn, fully automatically, complex temporal properties from execution traces. It is based on two insights:

(1) there is much regularity in the search space of learning all instances of a generic pattern, such as the alternating pattern (ab)*; 

(2) real, complex specifications can be formed by composing instances of small generic patterns. Javert can discover many interesting, nontrivial specifications in real-world code that are beyond the reach of existing automatic techniques.