Using Relational Verification for Program Slicing

Reviewed Paper In Proceedings

Author(s):Bernhard Beckert, Thorsten Bormer, Stephan Gocht, Mihai Herda, Daniel Lentzsch, and Mattias Ulbrich
In:17th International Conference on Software Engineering and Formal Methods (SEFM 2019)
Series:Lecture Notes in Computer Science


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.


    title       = {Using Relational Verification for Program Slicing},
    author      = {Bernhard Beckert and Thorsten Bormer and Stephan Gocht and Mihai Herda and Daniel Lentzsch and Mattias Ulbrich},
    editor      = {Peter {\"O}lveczky and Gwen Sala{\"u}n},
    booktitle   = {17th International Conference on Software Engineering and Formal Methods
                   ({SEFM} 2019)},
    series      = {Lecture Notes in Computer Science},
    volume      = {11724},
    year        = {2019},
    place       = {Oslo, Norway},
    date        = {September 16--20},
    month       = sep,
    pages       = {353--372},
    isbn        = {978-3-030-30446-1},
    doi         = {10.1007/978-3-030-30446-1_19}