Mining specications

Program verication is a promising approach to improving program quality, because it can search all possible program executions for specic errors. However, the need to formally describe correct be-havior or errors is a major barrier to the widespread adoption of program verication, since programmers historically have been re-luctant to write formal specications. Automating the process of formulating specications would remove a barrier to program ver-ication and enhance its practicality. This paper describes specication mining, a machine learning approach to discovering formal specications of the protocols that code must obey when interacting with an application program in-terface 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 specication by observing program execution and concisely summarizing the frequent inter-action patterns as state machines that capture both temporal and data dependences. These state machines can be examined by a pro-grammer, to rene the specication and identify errors, and can be utilized by automatic verication tools, to nd bugs. Our preliminary experience with the mining tool has been promising. We were able to learn specications that not only cap-tured the correct protocol, but also discovered serious bugs. 1