Theorem Prover Based Static Analyzer: Comparison Analysis Between ESC/Java2 and KeY

  • Aneesa Saeed
  • S. H. A. Hamid
Conference paper
Part of the Lecture Notes in Electrical Engineering book series (LNEE, volume 315)


Software developers utilize static analyzers to discover the defects in the software source code. One of the static analyzer categories is based on theorem prover. Due to the strength of the theorem prover in proving the programs correctness and soundness without producing false warnings, analysis on the verification tools is important to assess the performance. The objective of this paper is to analyze the performance of the open source theorem prover based static analyzers for Java. The analysis is done by comparing two static analyzers namely KeY and ESC/Java2 using four evaluation metrics for 20 test cases developed based on Common Weakness Enumeration (CWE). The result shows the performance of KeY is better than ESC/Java2 especially on Detection Coverage. The analysis also presents that the performances of theorem prover based static analyzers are effective on small developed benchmark only.


Static analysis Theorem prover Verification KeY ESC/java2 Software testing 



The authors acknowledge the support provided by University of Malaya Research Grant, RG10612ICT.


  1. 1.
    Luo, L.: Software Testing Techniques. Institute for software research international Carnegie Mellon University, Pittsburgh, 19 p (2001)Google Scholar
  2. 2.
    Díaz, G., Bermejo, J.R.: Static analysis of source code security: assessment of tools against SAMATE tests. Inf.Softw. Technol. 55(8), 1462–1476 (2013) Google Scholar
  3. 3.
    Chess, B., West, J.: Secure Programming with Static Analysis. Pearson Education, Boston (2007)Google Scholar
  4. 4.
    Young, M., Taylor, R.N.: Rethinking the taxonomy of fault detection techniques. In: Proceedings of 11th international conference on Software engineering, pp. 53–62. ACM (1989)Google Scholar
  5. 5.
    Cok, D.R., Kiniry, J.R.: Esc/java2: Uniting esc/java and jml. Construction and Analysis of Safe, Secure, and Interoperable Smart Devices, 3362,pp. 108–128. Springer (2005)Google Scholar
  6. 6.
    Beckert, B., Hähnle, R., Schmitt, P.H.: Verification of Object-Oriented Software: The KeY Approach. Springer, Berlin, Heidelberg (2007)Google Scholar
  7. 7.
    Meyer, J., Poetzsch-Heffter, A.: An architecture for interactive program provers. Tools and Algorithms for the Construction and Analysis of Systems,1785, pp. 63–77. Springer (2000)Google Scholar
  8. 8.
    Jacobs, B., Poll, E.: Java program verification at Nijmegen: Developments and perspective. Software Security-Theories and Systems, 3233, pp. 134–153. Springer (2004)Google Scholar
  9. 9.
    Distefano, D., Parkinson, J., jStar, M.J.: Towards practical verification for Java. ACM SIGPLAN Not. 43, 213–226 (2008)CrossRefGoogle Scholar
  10. 10.
    Jacobs, B., Smans, J., Piessens, F.: VeriFast: Imperative programs as proofs. In: VSTTE Workshop on Tools and Experiments. (2010)Google Scholar
  11. 11.
    Cuoq, P., Kirchner, F., Kosmatov, N., Prevosto, V., Signoles, J., Yakobowski, B.: Frama-C. Software Engineering and Formal Methods, pp. 233–247. Springer (2012)Google Scholar
  12. 12.
    Barnett, M., Chang, B.-Y.E., DeLine, R., Jacobs, B., Leino, K.R.M.: Boogie: a modular reusable verifier for object-oriented programs. In: Formal Methods for Components and Objects, 7504, pp. 364–387. Springer (2006)Google Scholar
  13. 13.
    Cok, D., Kiniry, J.: ESC/Java2: Uniting ESC/Java and JML. In: Barthe, G., Burdy, L., Huisman, M., Lanet, J.-L., Muntean, T. (eds.) Construction and Analysis of Safe, Secure, and Interoperable Smart Devices, vol. 3362, pp. 108–128. Springer, Berlin Heidelberg (2005)CrossRefGoogle Scholar
  14. 14.
    Albert, E., Bubel, R., Genaim, S., Hähnle, R., Puebla, G., Román-Díez, G.: Verified resource guarantees using COSTA and KeY. In: Proceedings of the 20th ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation. ACM, pp. 73–76 (2011)Google Scholar
  15. 15.
    Collavizza, H., Rueher, M., Van Hentenryck, P.: Comparison between CPBPV, ESC/JAVA, CBMC, BLAST, EUREKA and WHY for bounded program verification. arXiv preprint arXiv:0808. 1508 (2008)Google Scholar
  16. 16.
    Feinerer, I., Salzer, G.: A comparison of tools for teaching formal software verification. Formal Aspects Comput. 21, 293–301 (2009)CrossRefzbMATHGoogle Scholar
  17. 17.
    Rutar, N., Almazan, C.B., Foster, J.S.: A comparison of bug finding tools for Java. In: Software Reliability Engineering. 5th IEEE International Symposium on ISSRE, pp. 245–256 (2004)Google Scholar
  18. 18.
    Beckert, B., Bormer, T., Wagner, M.: A Metric for Testing Program Verification Systems, 7942, pp. 56–75. Tests and Proofs. Springer (2013)Google Scholar
  19. 19.
    Voigt, J., Irwin, W., Churcher, N.: Comparing and Evaluating Existing Software Contract Tools. Evaluation of Novel Approaches to Software Engineering, 275, pp. 49–63. Springer (2013)Google Scholar
  20. 20.
    Zheng, J., Williams, L., Nagappan, N., Snipes, W., Hudepohl, J.P., Vouk, M.A.: On the value of static analysis for fault detection in software. IEEE Trans. Softw. Eng. 32, 240–253 (2006)CrossRefGoogle Scholar
  21. 21.
    Copeland, T.: PMD Applied. Centennial Books, San Francisco (2005)Google Scholar
  22. 22.
    Burmester, S., Giese, H., Niere, J., Tichy, M., Wadsack, J.P., Wagner, R., Wendehals, L., Zündorf, A.: Tool integration at the meta-model level: the Fujaba approach. Int. J. Softw. Tools Technol. Transfer 6, 203–218 (2004)CrossRefGoogle Scholar
  23. 23.
    Hovemeyer, D., Pugh, W.: Finding bugs is easy. ACM SIGPLAN Not. 39, 92–106 (2004)CrossRefGoogle Scholar
  24. 24.
    Almossawi, A., Lim, K., Sinha, T.: Analysis Tool Evaluation: Coverity Prevent. Carnegie Mellon University, Pittsburgh (2006)Google Scholar
  25. 25.
  26. 26.
  27. 27.
    Flanagan, C., Leino, K.R.M., Lillibridge, M., Nelson, G., Saxe, J.B., Stata, R.: Extended static checking for Java, 37(5), pp. 234–245. ACM SIGPLAN Notices. ACM (2002) Google Scholar
  28. 28.
  29. 29.
    Manning, C.D., Raghavan, P., Schütze, H.: Introduction to Information Retrieval. Cambridge University Press, Cambridge (2008)Google Scholar

Copyright information

© Springer International Publishing Switzerland 2015

Authors and Affiliations

  1. 1.Faculty of Computer Science and Information TechnologyUniversity of MalayaKuala LumpurMalaysia

Personalised recommendations