{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,11]],"date-time":"2026-04-11T00:49:08Z","timestamp":1775868548066,"version":"3.50.1"},"reference-count":39,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[2018,1]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>\n            Program slicing can be used to reduce a given initial program to a smaller one (a\n            <jats:italic>slice<\/jats:italic>\n            ) that preserves the behavior of the initial program with respect to a chosen criterion. Verification and validation (V&amp;V) of software can become easier on slices, but require particular care in the presence of errors or non-termination in order to avoid unsound results or a poor level of code reduction in slices with respect to the initial program. This article proposes a theoretical foundation for conducting V&amp;V activities on a slice instead of the initial program. We introduce the notion of\n            <jats:italic>relaxed slicing<\/jats:italic>\n            that is still capable of producing small slices, even in the presence of errors or non-termination, and establish an appropriate soundness property. It allows us to give a precise interpretation of verification results (absence or presence of errors) obtained for a slice in terms of the initial program. The implementation of these results in the Coq proof assistant is presented and some of its difficult points are discussed.\n          <\/jats:p>","DOI":"10.1007\/s00165-017-0439-x","type":"journal-article","created":{"date-parts":[[2017,10,9]],"date-time":"2017-10-09T10:28:11Z","timestamp":1507544891000},"page":"107-131","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":5,"title":["Cut branches before looking for bugs: certifiably sound verification on relaxed slices"],"prefix":"10.1145","volume":"30","author":[{"given":"Jean-Christophe","family":"L\u00e9chenet","sequence":"first","affiliation":[{"name":"CEA, LIST, Software Reliability and Security Laboratory, PC 174, 91191, Gif-sur-Yvette, France"},{"name":"Laboratoire de Math\u00e9matiques et Informatique pour la Complexit\u00e9 et les Syst\u00e8mes,\u00a0 CentraleSup\u00e9lec, Universit\u00e9 Paris-Saclay, 91190, Gif-sur-Yvette, France"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Nikolai","family":"Kosmatov","sequence":"additional","affiliation":[{"name":"CEA, LIST, Software Reliability and Security Laboratory, PC 174, 91191, Gif-sur-Yvette, France"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Pascale","family":"Le Gall","sequence":"additional","affiliation":[{"name":"Laboratoire de Math\u00e9matiques et Informatique pour la Complexit\u00e9 et les Syst\u00e8mes,\u00a0 CentraleSup\u00e9lec, Universit\u00e9 Paris-Saclay, 91190, Gif-sur-Yvette, France"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","doi-asserted-by":"publisher","DOI":"10.1002\/spe.4380230603"},{"key":"e_1_2_1_2_2_2","doi-asserted-by":"crossref","unstructured":"Allen M Horwitz S (2003) Slicing Java programs that throw and catch exceptions. In: PEPM 2003 pp 44\u201354","DOI":"10.1145\/966049.777394"},{"key":"e_1_2_1_2_3_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.ipl.2007.10.002"},{"key":"e_1_2_1_2_4_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2009.10.025"},{"key":"e_1_2_1_2_5_2","doi-asserted-by":"publisher","DOI":"10.5555\/993954"},{"issue":"2","key":"e_1_2_1_2_6_2","doi-asserted-by":"crossref","first-page":"217","DOI":"10.1007\/s00165-011-0196-1","article-title":"Assertion-based slicing and slice graphs.","volume":"24","author":"Barros JB","year":"2012","journal-title":"Formal Asp Comput"},{"key":"e_1_2_1_2_7_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2006.01.012"},{"key":"e_1_2_1_2_8_2","unstructured":"Ball T Horwitz S (1993) Slicing programs with arbitrary control-flow. In: AADEBUG 1993"},{"key":"e_1_2_1_2_9_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0065-2458(03)62003-6"},{"key":"e_1_2_1_2_10_2","doi-asserted-by":"crossref","unstructured":"Blazy S Maroneze A Pichardie D (2015) Verified validation of program slicing. In: CPP 2015 pp 109\u2013117","DOI":"10.1145\/2676724.2693169"},{"key":"e_1_2_1_2_11_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10515-013-0127-x"},{"key":"e_1_2_1_2_12_2","doi-asserted-by":"crossref","unstructured":"Cartwright R Felleisen M (1989) The semantics of program dependence. In: PLDI 1989","DOI":"10.1145\/73141.74820"},{"key":"e_1_2_1_2_13_2","doi-asserted-by":"crossref","unstructured":"Chebaro O Kosmatov N Giorgetti A Julliand J (2011) The SANTE tool: value analysis program slicing and test generation for C program debugging. In: TAP 2011","DOI":"10.1007\/978-3-642-21768-5_7"},{"key":"e_1_2_1_2_14_2","doi-asserted-by":"crossref","unstructured":"Chebaro O Kosmatov N Giorgetti A Julliand J (2012) Program slicing enhances a verification technique combining static and dynamic analysis. In: SAC 2012","DOI":"10.1145\/2245276.2231980"},{"key":"e_1_2_1_2_15_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2011.08.033"},{"key":"e_1_2_1_2_16_2","doi-asserted-by":"publisher","DOI":"10.1023\/A:1025872819613"},{"key":"e_1_2_1_2_17_2","doi-asserted-by":"crossref","unstructured":"Ge X Taneja K Xie T Tillmann N (2011) DyTa: dynamic symbolic execution guided with static verification results. In: The 33rd international conference on software engineering (ICSE 2011) pp 992\u2013994. ACM","DOI":"10.1145\/1985793.1985971"},{"key":"e_1_2_1_2_18_2","doi-asserted-by":"publisher","DOI":"10.1002\/stvr.4370050303"},{"key":"e_1_2_1_2_19_2","doi-asserted-by":"publisher","DOI":"10.1002\/(SICI)1099-1689(199912)9:4<233::AID-STVR191>3.0.CO;2-3"},{"key":"e_1_2_1_2_20_2","doi-asserted-by":"crossref","unstructured":"Horwitz S Reps T Binkley D (1988) Interprocedural slicing using dependence graphs. In: PLDI 1988","DOI":"10.1145\/53990.53994"},{"key":"e_1_2_1_2_21_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF01213536"},{"key":"e_1_2_1_2_22_2","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-014-0326-7"},{"key":"e_1_2_1_2_23_2","doi-asserted-by":"crossref","unstructured":"Kiss B Kosmatov N Pariente D Puccetti A (2015) Combining static and dynamic analyses for vulnerability detection: illustration on Heartbleed. In: HVC 2015","DOI":"10.1007\/978-3-319-26287-1_3"},{"key":"e_1_2_1_2_24_2","unstructured":"L\u00e9chenet Jean-Christophe (2016) Formalization of relaxed slicing. http:\/\/perso.ecp.fr\/~lechenetjc\/slicing\/."},{"key":"e_1_2_1_2_25_2","doi-asserted-by":"publisher","DOI":"10.1145\/1538788.1538814"},{"key":"e_1_2_1_2_26_2","doi-asserted-by":"crossref","unstructured":"L\u00e9chenet J-C Kosmatov N Gall PL (2016) Cut branches before looking for bugs: Sound verification on relaxed slices. In: FASE\u201916 (Part of ETAPS\u201916) pp 179\u2013196","DOI":"10.1007\/978-3-662-49665-7_11"},{"key":"e_1_2_1_2_27_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlap.2009.03.001"},{"key":"e_1_2_1_2_28_2","doi-asserted-by":"publisher","DOI":"10.1109\/32.58784"},{"key":"e_1_2_1_2_29_2","unstructured":"Pierce BC Casinghino C Gaboardi M Greenberg M Hri\u0163cu C Sj\u00f6berg V Yorgey B (2015) Software foundations 3.2 2015. http:\/\/www.cis.upenn.edu\/~bcpierce\/sf\/sf-3.2\/index.html."},{"key":"e_1_2_1_2_30_2","doi-asserted-by":"publisher","DOI":"10.1145\/1275497.1275502"},{"key":"e_1_2_1_2_31_2","doi-asserted-by":"crossref","unstructured":"Reps TW Yang W (1988) The semantics of program slicing. Technical report University of Wisconsin","DOI":"10.1007\/3-540-50940-2_47"},{"key":"e_1_2_1_2_32_2","doi-asserted-by":"crossref","unstructured":"Reps TW Yang W (1989) The semantics of program slicing and program integration. In: TAPSOFT 1989","DOI":"10.1007\/3-540-50940-2_47"},{"key":"e_1_2_1_2_33_2","doi-asserted-by":"publisher","DOI":"10.1145\/2187671.2187674"},{"key":"e_1_2_1_2_34_2","unstructured":"Tip F (1995) A survey of program slicing techniques. J Prog Lang 3(3)"},{"key":"e_1_2_1_2_35_2","unstructured":"Wasserrab D (2011) From formal semantics to verified slicing: a modular framework with applications in language based security. Ph.D. thesis Karlsruhe Institute of Technology"},{"key":"e_1_2_1_2_36_2","unstructured":"Weiser M (1981) Program slicing. In: ICSE 1981"},{"key":"e_1_2_1_2_37_2","doi-asserted-by":"publisher","DOI":"10.1145\/358557.358577"},{"key":"e_1_2_1_2_38_2","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.1984.5010248"},{"key":"e_1_2_1_2_39_2","doi-asserted-by":"publisher","DOI":"10.1145\/1050849.1050865"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00165-017-0439-x\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-017-0439-x.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-017-0439-x.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s00165-017-0439-x","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,7]],"date-time":"2022-01-07T06:55:31Z","timestamp":1641538531000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s00165-017-0439-x"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,1]]},"references-count":39,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2018,1]]}},"alternative-id":["10.1007\/s00165-017-0439-x"],"URL":"https:\/\/doi.org\/10.1007\/s00165-017-0439-x","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2018,1]]}}}