In this talk, I will present Javert, the first general specification mining framework that can learn, fully automatically, complex temporal properties from execution traces.

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.

Bio

Zhendong Su is a Professor and Chancellor's Fellow at University of California, Davis. He received his PhD in Computer Science from University of California, Berkeley. His research focuses on developing practical techniques and tools for improving software quality and
programming productivity. He serves as an Associate Editor for ACM Transactions on Software Engineering and Methodology (ACM TOSEM), co-chaired the 2009 Static Analysis Symposium (SAS), and is the program chair of the 2012 International Symposium on Software Testing and Analysis (ISSTA).

*Scientific host:* Fritz Henglein
*Administrative host:* Jette Møller

All are welcome. No registration required.