Mining specifications

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 inor 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 temp...

• Type: Conference
• Year: 2002
• Where: POPL
• Authors: Glenn Ammons, James R. Larus, Rastislav Bodík
• Keywords: Frequent Interaction Patterns, Inor Abstract Data, Machine Learning Approach, POPL 2002, Programming Languages