SemSlice: Exploiting Relational Verification for Automatic Program Slicing

  • Bernhard Beckert
  • Thorsten Bormer
  • Stephan Gocht
  • Mihai HerdaEmail author
  • Daniel Lentzsch
  • Mattias Ulbrich
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 10510)


We present SemSlice, a tool which automatically produces very precise slices for C routines. Slicing is the process of removing statements from a program such that defined aspects of its behavior are retained. For producing precise slices, i.e., slices that are close to the minimal number of statements, the program’s semantics must be considered. SemSlice is based on automatic relational regression verification, which SemSlice uses to select valid slices from a set of candidate slices. We present several approaches for producing candidates for precise slices. Evaluation shows that regression verification (based on coupling invariant inference) is a powerful tool for semantics-aware slicing: precise slices for typical slicing challenges can be found automatically and fast.


  1. 1.
    Barros, J.B., Da Cruz, D., Henriques, P.R., Pinto, J.S.: Assertion-based slicing and slice graphs. Formal Aspects Comput. 24(2), 217–248 (2012)MathSciNetCrossRefzbMATHGoogle Scholar
  2. 2.
    Barthe, G., Crespo, J.M., Kunz, C.: Relational verification using product programs. In: Butler, M., Schulte, W. (eds.) FM 2011. LNCS, vol. 6664, pp. 200–214. Springer, Heidelberg (2011). doi: 10.1007/978-3-642-21437-0_17 CrossRefGoogle Scholar
  3. 3.
    Binkley, D., Harman, M.: A survey of empirical results on program slicing. Adv. Comput. 62, 105–178 (2004)CrossRefGoogle Scholar
  4. 4.
    Canfora, G., Cimitile, A., De Lucia, A.: Conditioned program slicing. Inf. Softw. Technol. 40(11), 595–607 (1998)CrossRefGoogle Scholar
  5. 5.
    da Cruz, D., Henriques, P.R., Pinto, J.S.: Gamaslicer: an online laboratory for program verification and analysis. In: Proceedings of the Tenth Workshop on Language Descriptions, Tools and Applications. p. 3. ACM (2010)Google Scholar
  6. 6.
    Eranki, K.L., Moudgalya, K.M.: Program slicing technique: a novel approach to improve programming skills in novice learners. In: Proceedings of the Conference on Information Technology Education. pp. 160–165. ACM (2016)Google Scholar
  7. 7.
    Felsing, D., Grebing, S., Klebanov, V., Rümmer, P., Ulbrich, M.: Automating regression verification. In: Proceedings of the International Conference on Automated Software Engineering, ASE 2014, pp. 349–360. ACM (2014)Google Scholar
  8. 8.
    Field, J., Ramalingam, G., Tip, F.: Parametric program slicing. In: Proceedings of the Symposium on Principles of Programming Languages, pp. 379–392. ACM (1995)Google Scholar
  9. 9.
    Halder, R., Cortesi, A.: Abstract program slicing on dependence condition graphs. Sci. Comput. Program. 78(9), 1240–1263 (2013)CrossRefGoogle Scholar
  10. 10.
    Hojjat, H., Konečný, F., Garnier, F., Iosif, R., Kuncak, V., Rümmer, P.: A verification toolkit for numerical transition systems. In: Giannakopoulou, D., Méry, D. (eds.) FM 2012. LNCS, vol. 7436, pp. 247–251. Springer, Heidelberg (2012). doi: 10.1007/978-3-642-32759-9_21 CrossRefGoogle Scholar
  11. 11.
    Jaffar, J., Murali, V., Navas, J.A., Santosa, A.E.: Path-sensitive backward slicing. In: Miné, A., Schmidt, D. (eds.) SAS 2012. LNCS, vol. 7460, pp. 231–247. Springer, Heidelberg (2012). doi: 10.1007/978-3-642-33125-1_17 CrossRefGoogle Scholar
  12. 12.
    Kiefer, M., Klebanov, V., Ulbrich, M.: Relational program reasoning using compiler IR. In: Blazy, S., Chechik, M. (eds.) VSTTE 2016. LNCS, vol. 9971, pp. 149–165. Springer, Cham (2016). doi: 10.1007/978-3-319-48869-1_12 CrossRefGoogle Scholar
  13. 13.
    Komondoor, R.: Precise slicing in imperative programs via term-rewriting and abstract interpretation. In: Logozzo, F., Fähndrich, M. (eds.) SAS 2013. LNCS, vol. 7935, pp. 259–282. Springer, Heidelberg (2013). doi: 10.1007/978-3-642-38856-9_15 CrossRefGoogle Scholar
  14. 14.
    Lattner, C., Adve, V.: Llvm: A compilation framework for lifelong program analysis and transformation. In: International Symposium on Code Generation and Optimization, CGO 2004, pp. 75–86. IEEE (2004)Google Scholar
  15. 15.
    Martin, R.C.: Clean Code: A Handbook of Agile Software Craftsmanship, 1st edn. Prentice Hall PTR, Upper Saddle River, NJ (2008)Google Scholar
  16. 16.
    Mastroeni, I., Nikolić, Đ.: Abstract program slicing: from theory towards an implementation. In: Dong, J.S., Zhu, H. (eds.) ICFEM 2010. LNCS, vol. 6447, pp. 452–467. Springer, Heidelberg (2010). doi: 10.1007/978-3-642-16901-4_30 CrossRefGoogle Scholar
  17. 17.
    Ward, M.: Properties of slicing definitions. In: Ninth IEEE International Working Conference on Source Code Analysis and Manipulation, SCAM 2009, pp. 23–32. IEEE (2009)Google Scholar
  18. 18.
    Weiser, M.: Program slicing. In: Proceedings of the 5th International Conference on Software Engineering. pp. 439–449. IEEE Press (1981)Google Scholar

Copyright information

© Springer International Publishing AG 2017

Authors and Affiliations

  • Bernhard Beckert
    • 1
  • Thorsten Bormer
    • 1
  • Stephan Gocht
    • 1
  • Mihai Herda
    • 1
    Email author
  • Daniel Lentzsch
    • 1
  • Mattias Ulbrich
    • 1
  1. 1.Karlsruhe Institute of Technology (KIT)KarlsruheGermany

Personalised recommendations