Mining specifications

TLDR

Program verification can improve software quality by exhaustively searching all executions for errors, but the requirement to write formal specifications has limited its adoption because programmers are reluctant to produce them. The authors propose automating specification generation to remove this barrier and make program verification more practical. They build a specification‑mining tool that learns formal protocol state machines from observed program executions, capturing both temporal and data dependencies. The resulting state machines allow programmers to refine specifications and detect errors, and the tool has successfully uncovered serious bugs, indicating its promise.

Abstract

Program verification is a promising approach to improving program quality, because it can search all possible program executions for specific errors. However, the need to formally describe correct behavior or errors is a major barrier to the widespread adoption of program verification, since programmers historically have been reluctant to write formal specifications. Automating the process of formulating specifications would remove a barrier to program verification and enhance its practicality.This paper describes specification mining, a machine learning approach to discovering formal specifications of the protocols that code must obey when interacting with an application program interface or abstract data type. Starting from the assumption that a working program is well enough debugged to reveal strong hints of correct protocols, our tool infers a specification by observing program execution and concisely summarizing the frequent interaction patterns as state machines that capture both temporal and data dependences. These state machines can be examined by a programmer, to refine the specification and identify errors, and can be utilized by automatic verification tools, to find bugs.Our preliminary experience with the mining tool has been promising. We were able to learn specifications that not only captured the correct protocol, but also discovered serious bugs.