Skip to main content
SpringerLink
Log in

Evaluation of Program Slicing in Software Verification

  • Conference paper
  • First Online:
Integrated Formal Methods (IFM 2019)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 11918))

Included in the following conference series:

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.

This work has been supported by the Czech Science Foundation grant GA18-02177S.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Notes

  1. 1.

    https://github.com/mchalupa/cpachecker/tree/llvm-fixes2.

  2. 2.

    Detailed numbers for each configuration and subcategory can be found at: https://github.com/staticafi/symbiotic/releases/tag/ifm2019.

References

  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/12285707

    MATH  Google Scholar 

  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_7

    Chapter  Google Scholar 

  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_9

    Chapter  Google Scholar 

  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_16

    Chapter  Google Scholar 

  5. Beyer, D., Löwe, S., Wendler, P.: Reliable benchmarking: requirements and solutions. STTT 21(1), 1–29 (2019)

    Article  Google Scholar 

  6. Binkley, D.W., Gallagher, K.B.: Program slicing. In: Advances in Computers, vol. 43, pp. 1–50 (1996)

    Google Scholar 

  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. 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. 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_29

    Chapter  Google Scholar 

  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. Chebaro, O., et al.: Behind the scenes in SANTE: a combination of static and dynamic analyses. Autom. Softw. Eng. 21(1), 107–143 (2014)

    Article  Google Scholar 

  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_5

    Chapter  Google Scholar 

  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)

    Article  Google Scholar 

  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_20

    Chapter  Google Scholar 

  15. Harman, M., Hierons, R.M.: An overview of program slicing. Softw. Focus 2(3), 85–92 (2001)

    Article  Google Scholar 

  16. Hatcliff, J., Dwyer, M.B., Zheng, H.: Slicing software for model construction. Higher-Order Symb. Comput. 13(4), 315–353 (2000)

    Article  Google Scholar 

  17. Hind, M.: Pointer analysis: haven’t we solved this problem yet? In: PASTE 2001, pp. 54–61. ACM (2001)

    Google Scholar 

  18. Horwitz, S., Reps, T.W., Binkley, D.W.: Interprocedural slicing using dependence graphs. ACM Trans. Program. Lang. Syst. 12(1), 26–60 (1990)

    Article  Google Scholar 

  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. 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_31

    Chapter  MATH  Google Scholar 

  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)

    Article  MathSciNet  Google Scholar 

  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_32

    Chapter  Google Scholar 

  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_4

    Chapter  Google Scholar 

  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. 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_14

    Chapter  Google Scholar 

  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_27

    Chapter  Google Scholar 

  27. Lucia, A.D.: Program slicing: methods and applications. In: SCAM 2001, pp. 144–151. IEEE Computer Society (2001)

    Google Scholar 

  28. Mohapatra, D.P., Mall, R., Kumar, R.: An overview of slicing techniques for object-oriented programs. Informatica (Slovenia) 30(2), 253–277 (2006)

    MATH  Google Scholar 

  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_7

    Chapter  MATH  Google Scholar 

  30. Sabouri, H., Sirjani, M.: Slicing-based reductions for Rebeca. Electr. Notes Theor. Comput. Sci. 260, 209–224 (2010)

    Article  Google Scholar 

  31. Tip, F.: A survey of program slicing techniques. J. Prog. Lang. 3(3), 121–189 (1995)

    Google Scholar 

  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. 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)

    Article  Google Scholar 

  34. Vasudevan, S., Emerson, E.A., Abraham, J.A.: Improved verification of hardware designs through antecedent conditioned slicing. STTT 9(1), 89–101 (2007)

    Article  Google Scholar 

  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. Weiser, M.: Program slicing. IEEE Trans. Softw. Eng. 10(4), 352–357 (1984)

    Article  Google Scholar 

  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)

    Article  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Masaryk University, Brno, Czech Republic

    Marek Chalupa & Jan Strejček

Authors
  1. Marek Chalupa
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Jan Strejček
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Jan Strejček .

Editor information

Editors and Affiliations

  1. Chalmers University of Technology, Gothenburg, Sweden

    Wolfgang Ahrendt

  2. University of Oslo, Oslo, Norway

    Silvia Lizeth Tapia Tarifa

Rights and permissions

Reprints and permissions

Copyright information

© 2019 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Chalupa, M., Strejček, J. (2019). Evaluation of Program Slicing in Software Verification. In: Ahrendt, W., Tapia Tarifa, S. (eds) Integrated Formal Methods. IFM 2019. Lecture Notes in Computer Science(), vol 11918. Springer, Cham. https://doi.org/10.1007/978-3-030-34968-4_6

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-34968-4_6

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-34967-7

  • Online ISBN: 978-3-030-34968-4

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation