nach oben

Erschienen in:

2019 | OriginalPaper | Buchkapitel

Using Relational Verification for Program Slicing

verfasst von : Bernhard Beckert, Thorsten Bormer, Stephan Gocht, Mihai Herda, Daniel Lentzsch, Mattias Ulbrich

Erschienen in: Software Engineering and Formal Methods

Verlag: Springer International Publishing

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config

KI-gestützte Suche

Aus

Abstract

Program 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 minimal in size, the program’s semantics must be considered. Existing approaches that go beyond a syntactical analysis and do take the semantics into account are not fully automatic and require auxiliary specifications from the user. In this paper, we adapt relational verification to check whether a slice candidate obtained by removing some instructions from a program is indeed a valid slice. Based on this, we propose a framework for precise and automatic program slicing. As part of this framework, we present three strategies for the generation of slice candidates, and we show how dynamic slicing approaches – that interweave generating and checking slice candidates – can be used for this purpose. The framework can easily be extended with other strategies for generating slice candidates. We discuss the strengths and weaknesses of slicing approaches that use our framework.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Vorheriges Kapitel Reproducible Execution of POSIX Programs with DiOS

Nächstes Kapitel Local Nontermination Detection for Parallel C++ Programs

LLVM language reference manual. https://llvm.org/docs/LangRef.html. Accessed 06 Feb 2019

Agrawal, H., Horgan, J.R.: Dynamic program slicing. In: Proceedings of the ACM SIGPLAN 1990 Conference on Programming Language Design and Implementation, PLDI 1990, pp. 246–256. ACM, New York (1990). https://doi.org/10.1145/93542.93576

Barraclough, R.W., et al.: A trajectory-based strict semantics for program slicing. Theoret. Comput. Sci. 411(11), 1372–1386 (2010). https://doi.org/10.1016/j.tcs.2009.10.025MathSciNetCrossRefMATH

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). https://doi.org/10.1007/s00165-011-0196-1MathSciNetCrossRefMATH

Beckert, B., Bormer, T., Gocht, S., Herda, M., Lentzsch, D., Ulbrich, M.: SemSlice: exploiting relational verification for automatic program slicing. In: Polikarpova, N., Schneider, S. (eds.) IFM 2017. LNCS, vol. 10510, pp. 312–319. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-66845-1_20CrossRef

Beckert, B., Bormer, T., Gocht, S., Herda, M., Lentzsch, D., Ulbrich, M.: Evaluation data of SemSlice (2019). https://doi.org/10.5281/zenodo.3334571

Beckert, B., Bormer, T., Gocht, S., Herda, M., Lentzsch, D., Ulbrich, M.: Implementation of the SemSlice tool (2019). https://doi.org/10.5281/zenodo.3334553

Binkley, D., Harman, M.: A survey of empirical results on program slicing. In: Advances in Computers, vol. 62, pp. 105–178. Elsevier (2004). https://doi.org/10.1016/S0065-2458(03)62003-6

Canfora, G., Cimitile, A., Lucia, A.D.: Conditioned program slicing. Inf. Softw. Technol. 40(11–12), 595–607 (1998). https://doi.org/10.1016/S0950-5849(98)00086-XCrossRef

10.

Chung, I.S., Lee, W.K., Yoon, G.S., Kwon, Y.R.: Program slicing based on specification. In: Proceedings of the 2001 ACM Symposium on Applied Computing, SAC 2001, pp. 605–609. ACM, New York (2001). https://doi.org/10.1145/372202.372784

11.

Comuzzi, J.J., Hart, J.M.: Program slicing using weakest preconditions. In: Gaudel, M.-C., Woodcock, J. (eds.) FME 1996. LNCS, vol. 1051, pp. 557–575. Springer, Heidelberg (1996). https://doi.org/10.1007/3-540-60973-3_107CrossRef

12.

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, LDTA 2010, pp. 3:1–3:8. ACM, New York (2010). https://doi.org/10.1145/1868281.1868284

13.

De Angelis, E., Fioravanti, F., Pettorossi, A., Proietti, M.: Relational verification through horn clause transformation. In: Rival, X. (ed.) SAS 2016. LNCS, vol. 9837, pp. 147–169. Springer, Heidelberg (2016). https://doi.org/10.1007/978-3-662-53413-7_8CrossRef

14.

Felsing, D., Grebing, S., Klebanov, V., Rümmer, P., Ulbrich, M.: Automating regression verification. In: Proceedings of the 29th ACM/IEEE International Conference on Automated Software Engineering, ASE 2014, pp. 349–360. ACM (2014). https://doi.org/10.1145/2642937.2642987

15.

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). https://doi.org/10.1145/24039.24041CrossRefMATH

16.

Field, J., Ramalingam, G., Tip, F.: Parametric program slicing. In: Proceedings of the 22nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 1995, pp. 379–392. ACM, New York (1995). https://doi.org/10.1145/199448.199534

17.

Halder, R., Cortesi, A.: Abstract program slicing on dependence condition graphs. Sci. Comput. Program. 78(9), 1240–1263 (2013). https://doi.org/10.1016/j.scico.2012.05.007CrossRef

18.

Hall, R.J.: Automatic extraction of executable program subsets by simultaneous dynamic program slicing. Autom. Softw. Eng. 2(1), 33–53 (1995). https://doi.org/10.1007/BF00873408CrossRef

19.

Hammer, C., Snelting, G.: Flow-sensitive, context-sensitive, and object-sensitive information flow control based on program dependence graphs. Int. J. Inf. Secur. 8(6), 399–422 (2009). https://doi.org/10.1007/s10207-009-0086-1CrossRef

20.

Herda, M., Tyszberowicz, S., Beckert, B.: Using dependence graphs to assist verification and testing of information-flow properties. In: Dubois, C., Wolff, B. (eds.) TAP 2018. LNCS, vol. 10889, pp. 83–102. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-92994-1_5CrossRef

21.

Horwitz, S., Prins, J., Reps, T.: On the adequacy of program dependence graphs for representing programs. In: Proceedings of the 15th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 1988, pp. 146–157. ACM, New York (1988). https://doi.org/10.1145/73560.73573

22.

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). https://doi.org/10.1007/978-3-642-33125-1_17CrossRef

23.

Jaffar, J., Murali, V., Navas, J.A., Santosa, A.E.: TRACER: a symbolic execution tool for verification. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 758–766. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-31424-7_61CrossRef

24.

Kiefer, M., Klebanov, V., Ulbrich, M.: Relational program reasoning using compiler IR - combining static verification and dynamic analysis. J. Autom. Reason. 60(3), 337–363 (2017). https://doi.org/10.1007/s10817-017-9433-5MathSciNetCrossRefMATH

25.

Kirchner, F., Kosmatov, N., Prevosto, V., Signoles, J., Yakobowski, B.: Frama-c: a software analysis perspective. Formal Aspects Comput. 27(3), 573–609 (2015). https://doi.org/10.1007/s00165-014-0326-7MathSciNetCrossRef

26.

Klebanov, V., Rümmer, P., Ulbrich, M.: Automating regression verification of pointer programs by predicate abstraction. Formal Methods Syst. Des. 52(3), 229–259 (2018). https://doi.org/10.1007/s10703-017-0293-8CrossRefMATH

27.

Korel, B., Laski, J.W.: Dynamic program slicing. Inf. Process. Lett. 29(3), 155–163 (1988). https://doi.org/10.1016/0020-0190(88)90054-3CrossRefMATH

28.

Korel, B., Rilling, J.: Dynamic program slicing methods. Inf. Softw. Technol. 40(11–12), 647–659 (1998). https://doi.org/10.1016/S0950-5849(98)00089-5CrossRef

29.

Léchenet, J.-C., Kosmatov, N., Le Gall, P.: Cut branches before looking for bugs: sound verification on relaxed slices. In: Stevens, P., Wąsowski, A. (eds.) FASE 2016. LNCS, vol. 9633, pp. 179–196. Springer, Heidelberg (2016). https://doi.org/10.1007/978-3-662-49665-7_11CrossRef

30.

Liu, T., Tyszberowicz, S., Herda, M., Beckert, B., Grahl, D., Taghdiri, M.: Computing specification-sensitive abstractions for program verification. In: Fränzle, M., Kapur, D., Zhan, N. (eds.) SETTA 2016. LNCS, vol. 9984, pp. 101–117. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-47677-3_7CrossRef

31.

Lucia, A.D.: Program slicing: methods and applications. In: Proceedings First IEEE International Workshop on Source Code Analysis and Manipulation, pp. 142–149, November 2001. https://doi.org/10.1109/SCAM.2001.972675

32.

de Moura, L., Bjørner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-78800-3_24CrossRef

33.

Podgurski, A., Clarke, L.A.: A formal model of program dependences and its implications for software testing, debugging, and maintenance. IEEE Trans. Softw. Eng. 16(9), 965–979 (1990). https://doi.org/10.1109/32.58784CrossRef

34.

Ranganath, V.P., Amtoft, T., Banerjee, A., Hatcliff, J., Dwyer, M.B.: A new foundation for control dependence and slicing for modern program structures. ACM Trans. Program. Lang. Syst. 29(5) (2007). https://doi.org/10.1145/1275497.1275502CrossRef

35.

Rümmer, P., Hojjat, H., Kuncak, V.: Disjunctive interpolants for horn-clause verification. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 347–363. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-39799-8_24CrossRef

36.

Snelting, G., Robschink, T., Krinke, J.: Efficient path conditions in dependence graphs for software safety analysis. ACM Trans. Softw. Eng. Methodol. 15(4), 410–457 (2006). https://doi.org/10.1145/1178625.1178628CrossRef

37.

Tip, F.: A survey of program slicing techniques. Technical report, Amsterdam, The Netherlands, The Netherlands (1994). https://www.franktip.org/pubs/jpl1995.pdf

38.

Verdoolaege, S., Janssens, G., Bruynooghe, M.: Equivalence checking of static affine programs using widening to handle recurrences. ACM Trans. Program. Lang. Syst. 34(3), 11:1–11:35 (2012). https://doi.org/10.1145/2362389.2362390CrossRefMATH

39.

Ward, M.: Properties of slicing definitions. In: 2009 Ninth IEEE International Working Conference on Source Code Analysis and Manipulation, pp. 23–32, September 2009. https://doi.org/10.1109/SCAM.2009.12

40.

Weiser, M.: Program slicing. In: Proceedings of the 5th International Conference on Software Engineering, ICSE 1981, Piscataway, NJ, USA, pp. 439–449. IEEE Press (1981). http://dl.acm.org/citation.cfm?id=800078.802557

41.

Xu, B., Qian, J., Zhang, X., Wu, Z., Chen, L.: A brief survey of program slicing. SIGSOFT Softw. Eng. Notes 30(2), 1–36 (2005). https://doi.org/10.1145/1050849.1050865CrossRef

Titel: Using Relational Verification for Program Slicing
verfasst von: Bernhard Beckert
Thorsten Bormer
Stephan Gocht
Mihai Herda
Daniel Lentzsch
Mattias Ulbrich
Verlag: Springer International Publishing
Buch: Software Engineering and Formal Methods
Print ISBN: 978-3-030-30445-4

Electronic ISBN: 978-3-030-30446-1

Copyright-Jahr: 2019
DOI: https://doi.org/10.1007/978-3-030-30446-1_19

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Premium Partner