{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,11]],"date-time":"2026-04-11T00:48:56Z","timestamp":1775868536953,"version":"3.50.1"},"reference-count":21,"publisher":"Association for Computing Machinery (ACM)","issue":"2","license":[{"start":{"date-parts":[[2012,3,1]],"date-time":"2012-03-01T00:00:00Z","timestamp":1330560000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[2012,3]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>This paper revisits the idea of slicing programs based on their axiomatic semantics, rather than using criteria based on control\/data dependencies. We show how the forward propagation of preconditions and the backward propagation of postconditions can be combined in a new slicing algorithm that is more precise than the existing specification-based algorithms. The algorithm is based on (a) a precise test for removable statements, and (b) the construction of a<jats:italic>slice graph<\/jats:italic>, a program control flow graph extended with semantic labels and additional edges that \u201cshort-circuit\u201d removable commands. It improves on previous approaches in two aspects: it does not fail to identify removable commands; and it produces the smallest possible slice that can be obtained (in a sense that will be made precise). Iteration is handled through the use of loop invariants and variants to ensure termination. The paper also discusses in detail applications of these forms of slicing, including the elimination of (conditionally) unreachable and dead code, and compares them to other related notions.<\/jats:p>","DOI":"10.1007\/s00165-011-0196-1","type":"journal-article","created":{"date-parts":[[2011,9,22]],"date-time":"2011-09-22T11:04:15Z","timestamp":1316689455000},"page":"217-248","source":"Crossref","is-referenced-by-count":9,"title":["Assertion-based slicing and slice graphs"],"prefix":"10.1145","volume":"24","author":[{"given":"Jos\u00e9 Bernardo","family":"Barros","sequence":"first","affiliation":[{"name":"Departamento de Inform\u00e1tica\/CCTC, Universidade do Minho, Campus de Gualtar, 4710-057, Braga, Portugal"}]},{"given":"Daniela","family":"da Cruz","sequence":"additional","affiliation":[{"name":"Departamento de Inform\u00e1tica\/CCTC, Universidade do Minho, Campus de Gualtar, 4710-057, Braga, Portugal"}]},{"given":"Pedro Rangel","family":"Henriques","sequence":"additional","affiliation":[{"name":"Departamento de Inform\u00e1tica\/CCTC, Universidade do Minho, Campus de Gualtar, 4710-057, Braga, Portugal"}]},{"given":"Jorge Sousa","family":"Pinto","sequence":"additional","affiliation":[{"name":"Departamento de Inform\u00e1tica\/CCTC, Universidade do Minho, Campus de Gualtar, 4710-057, Braga, Portugal"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10270-004-0058-x"},{"key":"e_1_2_1_2_2_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-004-0167-4"},{"key":"e_1_2_1_2_3_2","first-page":"364","volume-title":"FMCO, Lecture Notes in Computer Science, vol 4111","author":"Barnett M","year":"2005"},{"key":"e_1_2_1_2_4_2","unstructured":"Baudin P Cuoq P Filli\u00e2tre J-C March\u00e9 C Monate B Moy Y Prevosto V (2010) ACSL: ANSI\/ISO C Specification Language. CEA LIST and INRIA"},{"key":"e_1_2_1_2_5_2","doi-asserted-by":"crossref","unstructured":"Barros J da Cruz D Henriques PR Pinto JS (2010) Assertion-based slicing and slice graphs. In: Fiadeiro JL Gnesi S (eds) Proceedings of the 8th IEEE international conference on software engineering and formal methods (SEFM\u201910). IEEE Computer Society pp 93\u2013102","DOI":"10.1109\/SEFM.2010.18"},{"key":"e_1_2_1_2_6_2","doi-asserted-by":"crossref","unstructured":"Barnett M Rustan K Leino M Schulte W (2004) The Spec# programming system: an overview. In: CASSIS: construction and analysis of safe secure and interoperable smart devices Lecture Notes in Computer Science vol 3362. Springer Berlin pp 49\u201369","DOI":"10.1007\/978-3-540-30569-9_3"},{"key":"e_1_2_1_2_7_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0950-5849(98)00086-X"},{"key":"e_1_2_1_2_8_2","doi-asserted-by":"crossref","unstructured":"Comuzzi JJ Hart JM (1996) Program slicing using weakest preconditions. In: FME \u201996: Proceedings of the third international symposium of formal methods Europe on industrial benefit and advances in formal methods. Springer London pp 557\u2013575","DOI":"10.1007\/3-540-60973-3_107"},{"key":"e_1_2_1_2_9_2","doi-asserted-by":"crossref","unstructured":"Chung IS Lee WK Yoon GS Kwon YR (2001) Program slicing based on specification. In: SAC \u201901: Proceedings of the 2001 ACM symposium on applied computing. ACM New York pp 605\u2013609","DOI":"10.1145\/372202.372784"},{"key":"e_1_2_1_2_10_2","unstructured":"da Cruz D Henriques PR Pinto JS (2011) Verification graphs for programs with contracts (Submitted for publication)"},{"key":"e_1_2_1_2_11_2","doi-asserted-by":"crossref","unstructured":"da Cruz D Henriques PR Pinto JS (2010) Gamaslicer: an online laboratory for program verification and analysis. In: LDTA \u201910: Proceedings of the tenth workshop on language descriptions tools and applications. ACM New York pp 1\u20138","DOI":"10.1145\/1868281.1868284"},{"key":"e_1_2_1_2_12_2","unstructured":"Dijkstra EW (1976) A discipline of programming. Prentice-Hall Englewood Cliffs"},{"key":"e_1_2_1_2_13_2","unstructured":"Fox C Danicic S Harman M Hierons RM (2001) Backward conditioning: a new program specialisation technique and its application to program comprehension. In: Proceedings of the 9th international workshop on program comprehension (IWPC\u201901). IEEE Computer Society pp 89\u201397"},{"key":"e_1_2_1_2_14_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.cosrev.2011.02.002"},{"key":"e_1_2_1_2_15_2","doi-asserted-by":"crossref","unstructured":"Flanagan C Saxe JB (2001) Avoiding exponential explosion: generating compact verification conditions. In: POPL \u201901: Proceedings of the 28th ACM SIGPLAN-SIGACT symposium on principles of programming languages. ACM New York pp 193\u2013205","DOI":"10.1145\/360204.360220"},{"key":"e_1_2_1_2_16_2","doi-asserted-by":"crossref","unstructured":"Harman M Hierons RM Fox C Danicic S Howroyd J (2001) Pre\/post conditioned slicing. In: Proceedings of the IEEE international conference on software maintenance (ICSM\u201901). IEEE Computer Society pp 138\u2013147","DOI":"10.1109\/ICSM.2001.972724"},{"key":"e_1_2_1_2_17_2","doi-asserted-by":"publisher","DOI":"10.1145\/363235.363259"},{"key":"e_1_2_1_2_18_2","doi-asserted-by":"crossref","unstructured":"Meyer B (1992) Applying \u201cDesign by contract\u201d. IEEE Comput 25(10)","DOI":"10.1109\/2.161279"},{"key":"e_1_2_1_2_19_2","doi-asserted-by":"crossref","unstructured":"Ward M (2009) Properties of slicing definitions. In: SCAM \u201909: Proceedings of the 2009 ninth IEEE international working conference on source code analysis and manipulation. IEEE Computer Society Washington pp 23\u201332","DOI":"10.1109\/SCAM.2009.12"},{"key":"e_1_2_1_2_20_2","unstructured":"Weiser M (1981) Program slicing. In: ICSE \u201981: Proceedings of the 5th international conference on software engineering. IEEE Press Piscataway pp 439\u2013449"},{"key":"e_1_2_1_2_21_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\/content\/pdf\/10.1007\/s00165-011-0196-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00165-011-0196-1\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s00165-011-0196-1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,11]],"date-time":"2025-03-11T20:12:35Z","timestamp":1741723955000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s00165-011-0196-1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,3]]},"references-count":21,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2012,3]]}},"alternative-id":["10.1007\/s00165-011-0196-1"],"URL":"https:\/\/doi.org\/10.1007\/s00165-011-0196-1","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012,3]]}}}