Classifying Bugs with Interpolants

  • Andreas Podelski
  • Martin SchäfEmail author
  • Thomas Wies
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 9762)


We present an approach to the classification of error messages in the context of static checking in the style of ESC/Java. The idea is to compute a semantics-based signature for each error message and then group together error messages with the same signature. The approach aims at exploiting modern verification techniques based on, e.g., Craig interpolation in order to generate small but significant signatures. We have implemented the approach and applied it to three benchmark sets (from Apache Ant, Apache Cassandra, and our own tool). Our experiments indicate an interesting practical potential. More than half of the considered error messages (for procedures with more than just one error message) can be grouped together with another error message.


Error Signature Error Message Static Checker Verification Problem Error 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.



This work is funded in parts by AFRL contract No. FA8750-15-C-0010 and the National Science Foundation under grant CCF-1350574.


  1. 1.
    Anvik, J., Hiew, L., Murphy, G.C.: Who should fix this bug? In: ICSE, pp. 361–370. ACM (2006)Google Scholar
  2. 2.
    Arlt, S., Rubio-González, C., Rümmer, P., Schäf, M., Shankar, N.: The gradual verifier. In: Badger, J.M., Rozier, K.Y. (eds.) NFM 2014. LNCS, vol. 8430, pp. 313–327. Springer, Heidelberg (2014)CrossRefGoogle Scholar
  3. 3.
    Ball, T., Naik, M., Rajamani, S.K.: From symptom to cause: localizing errors in counterexample traces. SIGPLAN Not. 38, 97–105 (2003)CrossRefGoogle Scholar
  4. 4.
    Barnett, M., Fähndrich, M., Leino, K.R.M., Müller, P., Schulte, W., Venter, H.: Specification and verification: the Spec# experience. Commun. ACM 54(6), 81–91 (2011)CrossRefGoogle Scholar
  5. 5.
    Tabaei Befrouei, M., Wang, C., Weissenbacher, G.: Abstraction and mining of traces to explain concurrency bugs. In: Bonakdarpour, B., Smolka, S.A. (eds.) RV 2014. LNCS, vol. 8734, pp. 162–177. Springer, Heidelberg (2014)Google Scholar
  6. 6.
    Chang, C., Keisler, H.J.: Model Theory. Studies in Logic and the Foundations of Mathematics. Elsevier Science, North-Holland (1990)zbMATHGoogle Scholar
  7. 7.
    Christ, J., Ermis, E., Schäf, M., Wies, T.: Flow-sensitive fault localization. In: Giacobazzi, R., Berdine, J., Mastroeni, I. (eds.) VMCAI 2013. LNCS, vol. 7737, pp. 189–208. Springer, Heidelberg (2013)CrossRefGoogle Scholar
  8. 8.
    Cok, D.R.: OpenJML: JML for Java 7 by extending OpenJDK. In: Bobaru, M., Havelund, K., Holzmann, G.J., Joshi, R. (eds.) NFM 2011. LNCS, vol. 6617, pp. 472–479. Springer, Heidelberg (2011)CrossRefGoogle Scholar
  9. 9.
    Cousot, P., Cousot, R.: Systematic design of program analysis frameworks. In: POPL, pp. 269–282. ACM (1979)Google Scholar
  10. 10.
    Cousot, P., Cousot, R., Fähndrich, M., Logozzo, F.: Automatic inference of necessary preconditions. In: Giacobazzi, R., Berdine, J., Mastroeni, I. (eds.) VMCAI 2013. LNCS, vol. 7737, pp. 128–148. Springer, Heidelberg (2013)CrossRefGoogle Scholar
  11. 11.
    Dijkstra, E.W.: A Discipline of Programming. Prentice-Hall, Englewood Cliffs (1976)zbMATHGoogle Scholar
  12. 12.
    Dillig, I., Dillig, T., Aiken, A.: Automated error diagnosis using abductive inference. In: PLDI, pp. 181–192 (2012)Google Scholar
  13. 13.
    Ermis, E., Schäf, M., Wies, T.: Error invariants. In: Giannakopoulou, D., Méry, D. (eds.) FM 2012. LNCS, vol. 7436, pp. 187–201. Springer, Heidelberg (2012)CrossRefGoogle Scholar
  14. 14.
    Falke, S., Merz, F., Sinz, C.: LLBMC: improved bounded model checking of \(\sf C\) programs using LLVM. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013 (ETAPS 2013). LNCS, vol. 7795, pp. 623–626. Springer, Heidelberg (2013)CrossRefGoogle Scholar
  15. 15.
    Flanagan, C., Leino, K.R.M., Lillibridge, M., Nelson, G., Saxe, J.B., Stata, R.: Extended static checking for Java. SIGPLAN Not. 37, 234–245 (2002)CrossRefGoogle Scholar
  16. 16.
    Gupta, A., Henzinger, T.A., Radhakrishna, A., Samanta, R., Tarrach, T.: Succinct representation of concurrent trace sets. In: POPL, pp. 433–444. ACM (2015)Google Scholar
  17. 17.
    Heizmann, M., Hoenicke, J., Podelski, A.: Software model checking for people who love automata. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 36–52. Springer, Heidelberg (2013)CrossRefGoogle Scholar
  18. 18.
    Jin, W., Orso, A.: Bugredux: reproducing field failures for in-house debugging. In: ICSE, pp. 474–484. IEEE (2012)Google Scholar
  19. 19.
    Kremenek, T., Engler, D.: Z-ranking: using statistical analysis to counter the impact of static analysis approximations. In: SAS, pp. 295–315 (2003)Google Scholar
  20. 20.
    Kroening, D., Tautschnig, M.: CBMC – C bounded model checker. In: Ábrahám, E., Havelund, K. (eds.) TACAS 2014 (ETAPS). LNCS, vol. 8413, pp. 389–391. Springer, Heidelberg (2014)CrossRefGoogle Scholar
  21. 21.
    Lal, A., Qadeer, S.: Powering the static driver verifier using corral. In: FSE, pp. 202–212. ACM (2014)Google Scholar
  22. 22.
    Le, W., Soffa, M.L.: Path-based fault correlations. In: FSE, pp. 307–316 (2010)Google Scholar
  23. 23.
    Lee, W., Lee, W., Yi, K.: Sound non-statistical clustering of static analysis alarms. In: Kuncak, V., Rybalchenko, A. (eds.) VMCAI 2012. LNCS, vol. 7148, pp. 299–314. Springer, Heidelberg (2012)CrossRefGoogle Scholar
  24. 24.
    McMillan, K.L.: An interpolating theorem prover. Theor. Comput. Sci. 345, 101–121 (2005)MathSciNetCrossRefzbMATHGoogle Scholar
  25. 25.
    Murali, V., Sinha, N., Torlak, E., Chandra, S.: What gives? a hybrid algorithm for error trace explanation. In: Giannakopoulou, D., Kroening, D. (eds.) VSTTE 2014. LNCS, vol. 8471, pp. 270–286. Springer, Heidelberg (2014)Google Scholar
  26. 26.
    Nelson, G.: A generalization of Dijkstra’s calculus. ACM Trans. Program. Lang. Syst. 11(4), 517–561 (1989)CrossRefGoogle Scholar
  27. 27.
    Pacheco, C., Ernst, M.D.: Randoop: feedback-directed random testing for java. In: Companion to the 22nd ACM SIGPLAN Conference on Object-oriented Programming Systems and Applications Companion, OOPSLA 2007, New York, NY, USA, pp. 815–816. ACM (2007)Google Scholar
  28. 28.
    Rümmer, P.: A constraint sequent calculus for first-order logic with linear integer arithmetic. In: Cervesato, I., Veith, H., Voronkov, A. (eds.) LPAR 2008. LNCS (LNAI), vol. 5330, pp. 274–289. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  29. 29.
    Sankaranarayanan, S., Sipma, H., Manna, Z.: Non-linear loop invariant generation using Gröbner bases. In: POPL, pp. 318–329. ACM (2004)Google Scholar
  30. 30.
    Wang, X., Zhang, L., Xie, T., Anvik, J., Sun, J.: An approach to detecting duplicate bug reports using natural language and execution information. In: ICSE, pp. 461–470. ACM (2008)Google Scholar
  31. 31.
    Zeller, A.: Isolating cause-effect chains from computer programs. In: SIGSOFT FSE, pp. 1–10 (2002)Google Scholar

Copyright information

© Springer International Publishing Switzerland 2016

Authors and Affiliations

  1. 1.University of FreiburgFreiburg im BreisgauGermany
  2. 2.SRI InternationalMenlo ParkUSA
  3. 3.New York UniversityNew YorkUSA

Personalised recommendations