Copenhagen Programming Language
Fully Automatic Mining of General Temporal PropertiesZhendon
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)
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.
Fritz Henglein Administrative host:Jette Møller.
All are welcome.
The Copenhagen Programming
Language Seminar (COPLAS) is a collaboration between DIKU, DTU,
COPLAS is sponsored by the FIRST Graduate School.
To receive information about COPLAS talks by email, send a message to
firstname.lastname@example.org with the word 'subscribe' as subject or in the body.
For more information about COPLAS, see