DIKU IT-C RUC

COPLAS

Copenhagen Programming Language Seminar


Fully Automatic Mining of General Temporal PropertiesZhendon

Zhendong Su
University of California, Davis (UCD)

September 14th, 15:00 - 16:00
DIKU, Universitetsparken 1, Meeting room A+B (2-0-04 and 2-0-06)

Abstract:
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. In this talk, I 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 regulartiy in the search space of learning all instances of a generic pattern, such as the alternating pattern (ab)*; and 2) real, complex specifications can be formed by composing instances of small generic patterns. These motivate us to introduce a symbolic algorithm to exploit the regularity in learning generic patterns and sound inference rules to construct complex specifications from atomic patterns. Javert is general, precise, and scalable. It can discover many interesting, nontrivial specifications in real-world code that are beyond the reach of existing automatic techniques.

Scientific host: Fritz Henglein Administrative host:Jette Møller. All are welcome.
The Copenhagen Programming Language Seminar (COPLAS) is a collaboration between DIKU, DTU, ITU, and RUC.
COPLAS is sponsored by the FIRST Graduate School.
To receive information about COPLAS talks by email, send a message to prog-lang-request@mail.it-c.dk with the word 'subscribe' as subject or in the body.

For more information about COPLAS, see http://www.coplas.org