Specification Mining With Few False Positives

Formal specifications can help with program testing, optimization, refactoring, documentation, and, most importantly, debugging and repair. Unfortunately, formal specifications are difficult to write manually, while techniques that infer specifications automatically suffer from 90-99% false positive rates. Consequently, neither option is currently practical for most software development projects. The authors present a novel technique that automatically infers partial correctness specifications with a very low false positive rate. They claim that existing specification miners yield false positives because they assign equal weight to all aspects of program behavior. By using additional information from the software engineering process, they are able to dramatically reduce this rate.