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.


Error Detection Mining Technique Mining Algorithm Normal Trace Static Trace 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


  1. 1.
    Alur, R., Cerny, P., Madhusudan, P., Nam, W.: Synthesis of interface specifications for Java classes. Principles of Programming Languages (2005)Google Scholar
  2. 2.
    Ammons, G., Bodik, R., Larus, J.R.: Mining specifications. Principles of Programming Languages, 4–16 (2002)Google Scholar
  3. 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
  4. 4.
    Ball, T., Rajamani, S.K.: Automatically validating temporal safety properties of interfaces. In: Dwyer, M.B. (ed.) SPIN 2001. LNCS, vol. 2057, pp. 103–122. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  5. 5.
    Das, M., Lerner, S., Seigle, M.: ESP: path-sensitive program verification in polynomial time. SIGPLAN Notices 37(5), 57–68 (2002)CrossRefGoogle Scholar
  6. 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. 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. 8.
    Freedman, D., Pisani, R., Purves, R.: Statistics. W. W. Norton, New York (1998)Google Scholar
  9. 9.
    Hibernate. Object/relational mapping and transparent object persistence for Java and SQL databases (July 2004),
  10. 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. 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
  12. 12.
    Savage, S., Burrows, M., Nelson, G., Sobalvarro, P., Anderson, T.: Eraser: A dynamic data race detector for multithreaded programs. ACM Transactions on Computer Systems 15(4), 391–411 (1997)CrossRefGoogle Scholar
  13. 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. 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

Copyright information

© Springer-Verlag Berlin Heidelberg 2005

Authors and Affiliations

  • Westley Weimer
    • 1
  • George C. Necula
    • 1
  1. 1.University of CaliforniaBerkeley

Personalised recommendations