Mining Temporal Specifications for Error Detection
Specifications are necessary in order to find software bugs using program verification tools. This paper presents a novel automatic specification mining algorithm that uses information about error handling to learn temporal safety rules. Our algorithm is based on the observation that programs often make mistakes along exceptional control-flow paths, even when they behave correctly on normal execution paths. We show that this focus improves the effectiveness of the miner for discovering specifications beneficial for bug finding.
We present quantitative results comparing our technique to four existing miners. We highlight assumptions made by various miners that are not always born out in practice. Additionally, we apply our algorithm to existing Java programs and analyze its ability to learn specifications that find bugs in those programs. In our experiments, we find filtering candidate specifications to be more important than ranking them. We find 430 bugs in 1 million lines of code. Notably, we find 250 more bugs using per-program specifications learned by our algorithm than with generic specifications that apply to all programs.
KeywordsError Detection Mining Technique Mining Algorithm Normal Trace Static Trace
- 1.Alur, R., Cerny, P., Madhusudan, P., Nam, W.: Synthesis of interface specifications for Java classes. Principles of Programming Languages (2005)Google Scholar
- 2.Ammons, G., Bodik, R., Larus, J.R.: Mining specifications. Principles of Programming Languages, 4–16 (2002)Google Scholar
- 3.Ammons, G., Mandein, D., Bodik, R., Larus, J.: Debugging temporal specifications with concept analysis. In: Programming Language Design and Implementation, San Diego, California (June 2003)Google Scholar
- 6.DeLine, R., Fähndrich, M.: Enforcing high-level protocols in low-level software. Programming Language Design and Implementation, 59–69 (2001)Google Scholar
- 7.Engler, D.R., Chen, D.Y., Chou, A.: Bugs as inconsistent behavior: A general approach to inferring errors in systems code. In: Symposium on Operating Systems Principles, pp. 57–72 (2001)Google Scholar
- 8.Freedman, D., Pisani, R., Purves, R.: Statistics. W. W. Norton, New York (1998)Google Scholar
- 9.Hibernate. Object/relational mapping and transparent object persistence for Java and SQL databases (July 2004), http://www.hibernate.org/
- 10.Liblit, B., Aiken, A., Zheng, A.X., Jordan, M.I.: Bug isolation via remote program sampling. In: Programming Language Design and Implementation, San Diego, California, June 9–11 (2003)Google Scholar
- 11.Necula, G.C., McPeak, S., Weimer, W.: CCured: Type-safe retrofitting of legacy code. In: Principles of Programming Languages, pp. 128–139. ACM, New York (2002)Google Scholar
- 13.Weimer, W., Necula, G.: Finding and preventing run-time error handling mistakes. In: Object-Oriented Programming, Systems, Languages, and Applications, Vancouver, British Columbia, Canada (October 2004)Google Scholar
- 14.Whaley, J., Martin, M.C., Lam, M.S.: Automatic extraction of object-oriented component interfaces. In: International Symposium of Software Testing and Analysis (2002)Google Scholar