期刊
ACM SIGPLAN NOTICES
卷 37, 期 1, 页码 4-16出版社
ASSOC COMPUTING MACHINERY
DOI: 10.1145/565816.503275
关键词
-
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 specification, would remove a barrier to program verification and enhance its practicality. This paper describes specification mining, a machine learning approach to discovering formal specification, 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 identity 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.
作者
我是这篇论文的作者
点击您的名字以认领此论文并将其添加到您的个人资料中。
推荐
暂无数据