News

About SPECMATE

In the past decade, automated validation of software systems has made spectacular progresses. On the testing side, it is now possible to automatically generate test cases that effectively explore the entire program structure; on the verification side, we can now formally prove properties for software as complex as operating systems. To push validation further, however, we need specifications of what the software actually should do. But writing such specifications has always been hard—and so far significantly inhibited the deployment of rigorous development methods.

The SPECMATE methodology automatically extracts such specifications from existing systems, effectively leveraging the knowledge encoded into billions of code lines. SPECMATE starts with just an executable program (a) and automatically produces an incremental specification (b), starting with the most relevant properties; and a set of test cases fully covering the specification (c). Such specifications are ideal starting points for compositional modeling and verification, enabling the rigorous construction and derivation of new, safe, dependable software systems; they also widely automate development activities such as testing, defect detection, and program maintenance.

To achieve these goals, SPECMATE employs a combination of specification mining (extracting specifications from executions), test case generation (generating additional runs to explore execution space) and mutation analysis (seeding synthetic defects to assess test quality). The proposed techniques all scale to industrial-sized programs; all we need is the ability to execute individual functions.

The principal investigator, Andreas Zeller, is one of the world’s leading experts in automated debugging, mining software repositories, and dynamic program analysis. His recent breakthroughs in specification mining and software testing are what makes SPECMATE feasible.