Advertisement

Evaluation of Program Slicing in Software Verification

  • Marek Chalupa
  • Jan StrejčekEmail author
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11918)

Abstract

There are publications that consider the use of program slicing in software verification, but we are aware of no publication that thoroughly evaluates the impact of program slicing on the verification process. This paper aims to fill in this gap by providing a comparison of the effect of program slicing on the performance of the reachability analysis in several state-of-the-art software verification tools, namely CPAchecker, DIVINE, KLEE, SeaHorn, and SMACK. The effect of slicing is evaluated on the number of solved benchmarks and running times of the tools. Experiments show that the effect of program slicing is mostly positive and can significantly improve the performance of some tools.

References

  1. 1.
    Aho, A.V., Sethi, R., Ullman, J.D.: Compilers: Principles, Techniques, and Tools. Addison-Wesley Series in Computer Science/World Student Series Edition. Addison-Wesley, Boston (1986). http://www.worldcat.org/oclc/12285707zbMATHGoogle Scholar
  2. 2.
    Backes, J.D., Person, S., Rungta, N., Tkachuk, O.: Regression verification using impact summaries. In: Bartocci, E., Ramakrishnan, C.R. (eds.) SPIN 2013. LNCS, vol. 7976, pp. 99–116. Springer, Heidelberg (2013).  https://doi.org/10.1007/978-3-642-39176-7_7CrossRefGoogle Scholar
  3. 3.
    Beyer, D.: Automatic verification of C and Java programs: SV-COMP 2019. In: Beyer, D., Huisman, M., Kordon, F., Steffen, B. (eds.) TACAS 2019, Part III. LNCS, vol. 11429, pp. 133–155. Springer, Cham (2019).  https://doi.org/10.1007/978-3-030-17502-3_9CrossRefGoogle Scholar
  4. 4.
    Beyer, D., Keremoglu, M.E.: CPAchecker: a tool for configurable software verification. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 184–190. Springer, Heidelberg (2011).  https://doi.org/10.1007/978-3-642-22110-1_16CrossRefGoogle Scholar
  5. 5.
    Beyer, D., Löwe, S., Wendler, P.: Reliable benchmarking: requirements and solutions. STTT 21(1), 1–29 (2019)CrossRefGoogle Scholar
  6. 6.
    Binkley, D.W., Gallagher, K.B.: Program slicing. In: Advances in Computers, vol. 43, pp. 1–50 (1996)Google Scholar
  7. 7.
    Cadar, C., Dunbar, D., Engler, D.R.: KLEE: unassisted and automatic generation of high-coverage tests for complex systems programs. In: OSDI 2008, pp. 209–224. USENIX Association (2008)Google Scholar
  8. 8.
    Carter, M., He, S., Whitaker, J., Rakamaric, Z., Emmi, M.: SMACK software verification toolchain. In: ICSE 2016, pp. 589–592. ACM (2016)Google Scholar
  9. 9.
    Chalupa, M., Vitovská, M., Strejček, J.: SYMBIOTIC 5: boosted instrumentation. In: Beyer, D., Huisman, M. (eds.) TACAS 2018. LNCS, vol. 10806, pp. 442–446. Springer, Cham (2018).  https://doi.org/10.1007/978-3-319-89963-3_29CrossRefGoogle Scholar
  10. 10.
    Chebaro, O., Kosmatov, N., Giorgetti, A., Julliand, J.: Program slicing enhances a verification technique combining static and dynamic analysis. In: SAC 2012, pp. 1284–1291. ACM (2012)Google Scholar
  11. 11.
    Chebaro, O., et al.: Behind the scenes in SANTE: a combination of static and dynamic analyses. Autom. Softw. Eng. 21(1), 107–143 (2014)CrossRefGoogle Scholar
  12. 12.
    Dwyer, M.B., Hatcliff, J., Hoosier, M., Ranganath, V.P., Robby, Wallentine, T.: Evaluating the effectiveness of slicing for model reduction of concurrent object-oriented programs. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006. LNCS, pp. 73–89. Springer, Heidelberg (2006).  https://doi.org/10.1007/11691372_5CrossRefGoogle Scholar
  13. 13.
    Ferrante, J., Ottenstein, K.J., Warren, J.D.: The program dependence graph and its use in optimization. ACM Trans. Program. Lang. Syst. 9(3), 319–349 (1987)CrossRefGoogle Scholar
  14. 14.
    Gurfinkel, A., Kahsai, T., Komuravelli, A., Navas, J.A.: The SeaHorn verification framework. In: Kroening, D., Păsăreanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 343–361. Springer, Cham (2015).  https://doi.org/10.1007/978-3-319-21690-4_20CrossRefGoogle Scholar
  15. 15.
    Harman, M., Hierons, R.M.: An overview of program slicing. Softw. Focus 2(3), 85–92 (2001)CrossRefGoogle Scholar
  16. 16.
    Hatcliff, J., Dwyer, M.B., Zheng, H.: Slicing software for model construction. Higher-Order Symb. Comput. 13(4), 315–353 (2000)CrossRefGoogle Scholar
  17. 17.
    Hind, M.: Pointer analysis: haven’t we solved this problem yet? In: PASTE 2001, pp. 54–61. ACM (2001)Google Scholar
  18. 18.
    Horwitz, S., Reps, T.W., Binkley, D.W.: Interprocedural slicing using dependence graphs. ACM Trans. Program. Lang. Syst. 12(1), 26–60 (1990)CrossRefGoogle Scholar
  19. 19.
    Ivancic, F., et al.: Model checking C programs using F-SOFT. In: ICCD 2005, pp. 297–308. IEEE Computer Society (2005)Google Scholar
  20. 20.
    Ivančić, F., Yang, Z., Ganai, M.K., Gupta, A., Shlyakhter, I., Ashar, P.: F-Soft: software verification platform. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 301–306. Springer, Heidelberg (2005).  https://doi.org/10.1007/11513988_31CrossRefzbMATHGoogle Scholar
  21. 21.
    Ivancic, F., Yang, Z., Ganai, M.K., Gupta, A., Ashar, P.: Efficient SAT-based bounded model checking for software verification. Theor. Comput. Sci. 404(3), 256–274 (2008)MathSciNetCrossRefGoogle Scholar
  22. 22.
    Lal, A., Qadeer, S., Lahiri, S.K.: A solver for reachability modulo theories. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 427–443. Springer, Heidelberg (2012).  https://doi.org/10.1007/978-3-642-31424-7_32CrossRefGoogle Scholar
  23. 23.
    Lange, T., Neuhäußer, M.R., Noll, T.: Speeding up the safety verification of programmable logic controller code. In: Bertacco, V., Legay, A. (eds.) HVC 2013. LNCS, vol. 8244, pp. 44–60. Springer, Cham (2013).  https://doi.org/10.1007/978-3-319-03077-7_4CrossRefGoogle Scholar
  24. 24.
    Lattner, C., Adve, V.S.: LLVM: a compilation framework for lifelong program analysis & transformation. In: CGO 2004, pp. 75–88. IEEE Computer Society (2004)Google Scholar
  25. 25.
    Lauko, H., Štill, V., Ročkai, P., Barnat, J.: Extending DIVINE with symbolic verification using SMT. In: Beyer, D., Huisman, M., Kordon, F., Steffen, B. (eds.) TACAS 2019. LNCS, vol. 11429, pp. 204–208. Springer, Cham (2019).  https://doi.org/10.1007/978-3-030-17502-3_14CrossRefGoogle Scholar
  26. 26.
    Li, X., Hoover, H.J., Rudnicki, P.: Towards automatic exception safety verification. In: Misra, J., Nipkow, T., Sekerinski, E. (eds.) FM 2006. LNCS, vol. 4085, pp. 396–411. Springer, Heidelberg (2006).  https://doi.org/10.1007/11813040_27CrossRefGoogle Scholar
  27. 27.
    Lucia, A.D.: Program slicing: methods and applications. In: SCAM 2001, pp. 144–151. IEEE Computer Society (2001)Google Scholar
  28. 28.
    Mohapatra, D.P., Mall, R., Kumar, R.: An overview of slicing techniques for object-oriented programs. Informatica (Slovenia) 30(2), 253–277 (2006)zbMATHGoogle Scholar
  29. 29.
    Ranganath, V.P., Amtoft, T., Banerjee, A., Dwyer, M.B., Hatcliff, J.: A new foundation for control-dependence and slicing for modern program structures. In: Sagiv, M. (ed.) ESOP 2005. LNCS, vol. 3444, pp. 77–93. Springer, Heidelberg (2005).  https://doi.org/10.1007/978-3-540-31987-0_7CrossRefzbMATHGoogle Scholar
  30. 30.
    Sabouri, H., Sirjani, M.: Slicing-based reductions for Rebeca. Electr. Notes Theor. Comput. Sci. 260, 209–224 (2010)CrossRefGoogle Scholar
  31. 31.
    Tip, F.: A survey of program slicing techniques. J. Prog. Lang. 3(3), 121–189 (1995)Google Scholar
  32. 32.
    Trabish, D., Mattavelli, A., Rinetzky, N., Cadar, C.: Chopped symbolic execution. In: Proceedings of the 40th International Conference on Software Engineering, ICSE 2018, Gothenburg, Sweden, 27 May–03 June 2018, pp. 350–360. ACM (2018). https://doi.org/10.1145/3180155.3180251
  33. 33.
    Vasudevan, S., Emerson, E.A., Abraham, J.A.: Efficient model checking of hardware using conditioned slicing. Electr. Notes Theor. Comput. Sci. 128(6), 279–294 (2005)CrossRefGoogle Scholar
  34. 34.
    Vasudevan, S., Emerson, E.A., Abraham, J.A.: Improved verification of hardware designs through antecedent conditioned slicing. STTT 9(1), 89–101 (2007)CrossRefGoogle Scholar
  35. 35.
    Wang, L., Zhang, Q., Zhao, P.: Automated detection of code vulnerabilities based on program analysis and model checking. In: SCAM 2008, pp. 165–173. IEEE Computer Society (2008)Google Scholar
  36. 36.
    Weiser, M.: Program slicing. IEEE Trans. Softw. Eng. 10(4), 352–357 (1984)CrossRefGoogle Scholar
  37. 37.
    Xu, B., Qian, J., Zhang, X., Wu, Z., Chen, L.: A brief survey of program slicing. ACM SIGSOFT Softw. Eng. Notes 30(2), 1–36 (2005)CrossRefGoogle Scholar

Copyright information

© Springer Nature Switzerland AG 2019

Authors and Affiliations

  1. 1.Masaryk UniversityBrnoCzech Republic

Personalised recommendations