{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,5]],"date-time":"2025-10-05T04:36:56Z","timestamp":1759639016072,"version":"3.41.0"},"publisher-location":"Berlin, Heidelberg","reference-count":35,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783662496640"},{"type":"electronic","value":"9783662496657"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2016]]},"DOI":"10.1007\/978-3-662-49665-7_11","type":"book-chapter","created":{"date-parts":[[2016,3,21]],"date-time":"2016-03-21T08:09:42Z","timestamp":1458547782000},"page":"179-196","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["Cut Branches Before Looking for Bugs: Sound Verification on Relaxed Slices"],"prefix":"10.1007","author":[{"given":"Jean-Christophe","family":"L\u00e9chenet","sequence":"first","affiliation":[]},{"given":"Nikolai","family":"Kosmatov","sequence":"additional","affiliation":[]},{"given":"Pascale","family":"Le Gall","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"11_CR1","unstructured":"Formalization of relaxed slicing (2016). http:\/\/perso.ecp.fr\/~lechenetjc\/slicing\/"},{"issue":"6","key":"11_CR2","doi-asserted-by":"publisher","first-page":"589","DOI":"10.1002\/spe.4380230603","volume":"23","author":"H Agrawal","year":"1993","unstructured":"Agrawal, H., DeMillo, R.A., Spafford, E.H.: Debugging with dynamic slicing and backtracking. Softw. Pract. Exper. 23(6), 589\u2013616 (1993)","journal-title":"Softw. Pract. Exper."},{"issue":"10","key":"11_CR3","doi-asserted-by":"crossref","first-page":"44","DOI":"10.1145\/966049.777394","volume":"38","author":"Matthew Allen","year":"2003","unstructured":"Allen, M., Horwitz, S.: Slicing java programs that throw and catch exceptions. In: PEPM 2003, pp. 44\u201354 (2003)","journal-title":"ACM SIGPLAN Notices"},{"issue":"2","key":"11_CR4","doi-asserted-by":"publisher","first-page":"45","DOI":"10.1016\/j.ipl.2007.10.002","volume":"106","author":"T Amtoft","year":"2008","unstructured":"Amtoft, T.: Slicing for modern program structures: a theory for eliminating irrelevant loops. Inf. Process. Lett. 106(2), 45\u201351 (2008)","journal-title":"Inf. Process. Lett."},{"key":"11_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"206","DOI":"10.1007\/BFb0019410","volume-title":"Automated and Algorithmic Debugging","author":"T Ball","year":"1993","unstructured":"Ball, T., Horwitz, S.: Slicing programs with arbitrary control-flow. In: Fritzson, P.A. (ed.) AADEBUG 1993. LNCS, vol. 749, pp. 206\u2013222. Springer, Heidelberg (1993)"},{"issue":"11\u201313","key":"11_CR6","doi-asserted-by":"publisher","first-page":"1372","DOI":"10.1016\/j.tcs.2009.10.025","volume":"411","author":"RW Barraclough","year":"2010","unstructured":"Barraclough, R.W., Binkley, D., Danicic, S., Harman, M., Hierons, R.M., Kiss, A., Laurence, M., Ouarbya, L.: A trajectory-based strict semantics for program slicing. Theor. Comp. Sci. 411(11\u201313), 1372\u20131386 (2010)","journal-title":"Theor. Comp. Sci."},{"key":"11_CR7","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-07964-5","volume-title":"Interactive Theorem Proving and Program Development","author":"Y Bertot","year":"2004","unstructured":"Bertot, Y., Cast\u00e9ran, P.: Interactive Theorem Proving and Program Development. Springer, Heidelberg (2004)"},{"issue":"1\u20133","key":"11_CR8","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1016\/j.tcs.2006.01.012","volume":"360","author":"D Binkley","year":"2006","unstructured":"Binkley, D., Danicic, S., Gyim\u00f3thy, T., Harman, M., Kiss, \u00c1., Korel, B.: Theoretical foundations of dynamic program slicing. Theor. Comput. Sci. 360(1\u20133), 23\u201341 (2006)","journal-title":"Theor. Comput. Sci."},{"key":"11_CR9","doi-asserted-by":"publisher","first-page":"105","DOI":"10.1016\/S0065-2458(03)62003-6","volume":"62","author":"D Binkley","year":"2004","unstructured":"Binkley, D., Harman, M.: A survey of empirical results on program slicing. Adv. Comput. 62, 105\u2013178 (2004)","journal-title":"Adv. Comput."},{"key":"11_CR10","first-page":"109","volume":"2015","author":"S Blazy","year":"2015","unstructured":"Blazy, S., Maroneze, A., Pichardie, D.: Verified validation of program slicing. CPP 2015, 109\u2013117 (2015)","journal-title":"CPP"},{"key":"11_CR11","doi-asserted-by":"crossref","unstructured":"Cartwright, R., Felleisen, M.: The semantics of program dependence. In: PLDI (1989)","DOI":"10.1145\/73141.74820"},{"issue":"1","key":"11_CR12","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1007\/s10515-013-0127-x","volume":"21","author":"O Chebaro","year":"2014","unstructured":"Chebaro, O., Cuoq, P., Kosmatov, N., Marre, B., Pacalet, A., Williams, N., Yakobowski, B.: Behind the scenes in SANTE: a combination of static and dynamic analyses. Autom. Softw. Eng. 21(1), 107\u2013143 (2014)","journal-title":"Autom. Softw. Eng."},{"key":"11_CR13","doi-asserted-by":"crossref","unstructured":"Chebaro, O., Kosmatov, N., Giorgetti, A., Julliand, J.: Program slicing enhances a verification technique combining static and dynamic analysis. In: SAC (2012)","DOI":"10.1145\/2245276.2231980"},{"issue":"49","key":"11_CR14","doi-asserted-by":"publisher","first-page":"6809","DOI":"10.1016\/j.tcs.2011.08.033","volume":"412","author":"S Danicic","year":"2011","unstructured":"Danicic, S., Barraclough, R.W., Harman, M., Howroyd, J., Kiss, \u00c1., Laurence, M.R.: A unifying theory of control dependence and its application to arbitrary program structures. Theor. Comput. Sci. 412(49), 6809\u20136842 (2011)","journal-title":"Theor. Comput. Sci."},{"key":"11_CR15","doi-asserted-by":"crossref","unstructured":"Ge, X., Taneja, K., Xie, T., Tillmann, N.: DyTa: dynamic symbolic execution guided with static verification results. In: the 33rd International Conference on Software Engineering (ICSE 2011), pp. 992\u2013994. ACM (2011)","DOI":"10.1145\/1985793.1985971"},{"issue":"4","key":"11_CR16","doi-asserted-by":"publisher","first-page":"297","DOI":"10.1023\/A:1025872819613","volume":"16","author":"R Giacobazzi","year":"2003","unstructured":"Giacobazzi, R., Mastroeni, I.: Non-standard semantics for program slicing. High. Order Symbolic Comput. 16(4), 297\u2013339 (2003)","journal-title":"High. Order Symbolic Comput."},{"issue":"3","key":"11_CR17","doi-asserted-by":"publisher","first-page":"143","DOI":"10.1002\/stvr.4370050303","volume":"5","author":"M Harman","year":"1995","unstructured":"Harman, M., Danicic, S.: Using program slicing to simplify testing. Softw. Test. Verif. Reliab. 5(3), 143\u2013162 (1995)","journal-title":"Softw. Test. Verif. Reliab."},{"issue":"4","key":"11_CR18","doi-asserted-by":"publisher","first-page":"490","DOI":"10.1007\/BF01213536","volume":"8","author":"M Harman","year":"1996","unstructured":"Harman, M., Simpson, D., Danicic, S.: Slicing programs in the presence of errors. Formal Aspects Comput. 8(4), 490\u2013497 (1996)","journal-title":"Formal Aspects Comput."},{"issue":"4","key":"11_CR19","doi-asserted-by":"publisher","first-page":"233","DOI":"10.1002\/(SICI)1099-1689(199912)9:4<233::AID-STVR191>3.0.CO;2-3","volume":"9","author":"RM Hierons","year":"1999","unstructured":"Hierons, R.M., Harman, M., Danicic, S.: Using program slicing to assist in the detection of equivalent mutants. Softw. Test. Verif. Reliab. 9(4), 233\u2013262 (1999)","journal-title":"Softw. Test. Verif. Reliab."},{"issue":"7","key":"11_CR20","doi-asserted-by":"crossref","first-page":"35","DOI":"10.1145\/960116.53994","volume":"23","author":"S. Horwitz","year":"1988","unstructured":"Horwitz, S., Reps, T., Binkley, D.: Interprocedural slicing using dependence graphs. In: PLDI (1988)","journal-title":"ACM SIGPLAN Notices"},{"issue":"3","key":"11_CR21","doi-asserted-by":"publisher","first-page":"573","DOI":"10.1007\/s00165-014-0326-7","volume":"27","author":"F Kirchner","year":"2015","unstructured":"Kirchner, F., Kosmatov, N., Prevosto, V., Signoles, J., Yakobowski, B.: Frama-C: a software analysis perspective. Formal Asp. Comput. 27(3), 573\u2013609 (2015)","journal-title":"Formal Asp. Comput."},{"key":"11_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1007\/978-3-319-26287-1_3","volume-title":"Hardware and Software: Verification and Testing","author":"B Kiss","year":"2015","unstructured":"Kiss, B., Kosmatov, N., Pariente, D., Puccetti, A.: Combining static and dynamic analyses for vulnerability detection: illustration on heartbleed. In: Piterman, N., et al. (eds.) HVC 2015. LNCS, vol. 9434, pp. 39\u201350. Springer, Heidelberg (2015). doi: 10.1007\/978-3-319-26287-1_3"},{"issue":"7","key":"11_CR23","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1145\/1538788.1538814","volume":"52","author":"X Leroy","year":"2009","unstructured":"Leroy, X.: Formal verification of a realistic compiler. Commun. ACM 52(7), 107\u2013115 (2009)","journal-title":"Commun. ACM"},{"issue":"7","key":"11_CR24","doi-asserted-by":"publisher","first-page":"573","DOI":"10.1016\/j.jlap.2009.03.001","volume":"78","author":"H Nestra","year":"2009","unstructured":"Nestra, H.: Transfinite semantics in the form of greatest fixpoint. J. Log. Algebr. Program. 78(7), 573\u2013592 (2009)","journal-title":"J. Log. Algebr. Program."},{"issue":"9","key":"11_CR25","doi-asserted-by":"publisher","first-page":"965","DOI":"10.1109\/32.58784","volume":"16","author":"A Podgurski","year":"1990","unstructured":"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\u2013979 (1990)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"11_CR26","doi-asserted-by":"crossref","unstructured":"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). Article number (27)","DOI":"10.1145\/1275497.1275502"},{"key":"11_CR27","doi-asserted-by":"crossref","first-page":"360","DOI":"10.1007\/3-540-50940-2_47","volume-title":"TAPSOFT '89","author":"Thomas Reps","year":"1989","unstructured":"Reps, T.W., Yang, W.: The semantics of program slicing and program integration. In: TAPSOFT (1989)"},{"key":"11_CR28","doi-asserted-by":"crossref","unstructured":"Reps, T.W., Yang, W.: The semantics of program slicing. Technical report, University of Wisconsin (1988)","DOI":"10.1007\/3-540-50940-2_47"},{"issue":"3","key":"11_CR29","doi-asserted-by":"publisher","first-page":"12","DOI":"10.1145\/2187671.2187674","volume":"44","author":"J Silva","year":"2012","unstructured":"Silva, J.: A vocabulary of program slicing-based techniques. ACM Comput. Surv. 44(3), 12 (2012)","journal-title":"ACM Comput. Surv."},{"issue":"3","key":"11_CR30","first-page":"121","volume":"3","author":"F Tip","year":"1995","unstructured":"Tip, F.: A survey of program slicing techniques. J. Prog. Lang. 3(3), 121\u2013189 (1995)","journal-title":"J. Prog. Lang."},{"key":"11_CR31","unstructured":"Wasserrab, D.: From formal semantics to verified slicing: a modular framework with applications in language based security. Ph.D. thesis, Karlsruhe Inst. of Techn (2011)"},{"key":"11_CR32","unstructured":"Weiser, M.: Program slicing. In: ICSE (1981)"},{"issue":"7","key":"11_CR33","doi-asserted-by":"publisher","first-page":"446","DOI":"10.1145\/358557.358577","volume":"25","author":"M Weiser","year":"1982","unstructured":"Weiser, M.: Programmers use slices when debugging. Commun. ACM 25(7), 446\u2013452 (1982)","journal-title":"Commun. ACM"},{"issue":"4","key":"11_CR34","doi-asserted-by":"publisher","first-page":"352","DOI":"10.1109\/TSE.1984.5010248","volume":"10","author":"M Weiser","year":"1984","unstructured":"Weiser, M.: Program slicing. IEEE Trans. Softw. Eng. 10(4), 352\u2013357 (1984)","journal-title":"IEEE Trans. Softw. Eng."},{"issue":"2","key":"11_CR35","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/1050849.1050865","volume":"30","author":"B Xu","year":"2005","unstructured":"Xu, B., Qian, J., Zhang, X., Wu, Z., Chen, L.: A brief survey of program slicing. ACM SIGSOFT Softw. Eng. Notes 30(2), 1\u201336 (2005)","journal-title":"ACM SIGSOFT Softw. Eng. Notes"}],"container-title":["Lecture Notes in Computer Science","Fundamental Approaches to Software Engineering"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-49665-7_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,1]],"date-time":"2025-06-01T21:29:18Z","timestamp":1748813358000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-662-49665-7_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783662496640","9783662496657"],"references-count":35,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-49665-7_11","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2016]]},"assertion":[{"value":"This content has been made available to all.","name":"free","label":"Free to read"}]}}