Title
Assertion-based slicing and slice graphs
Abstract
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 slice graph, a program control flow graph extended with semantic labels and additional edges that “short-circuit” 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.
Year
DOI
Venue
2010
10.1007/s00165-011-0196-1
Software Engineering and Formal Methods
Keywords
Field
DocType
removable statement,smallest possible slice,existing specification-based algorithm,precise test,removable command,additional edge,forward propagation,program control flow graph,axiomatic semantics,slice graph,program analysis
Program slicing,Axiomatic semantics,Control flow graph,Computer science,Slicing,Assertion,Algorithm,Theoretical computer science,Loop invariant,Program analysis,Dead code
Conference
Volume
Issue
ISSN
24
2
1433-299X
ISBN
Citations 
PageRank 
978-1-4244-8289-4
6
0.44
References 
Authors
8
4
Name
Order
Citations
PageRank
José Bernardo Barros160.44
Daniela da Cruz293.19
Pedro Rangel Henriques327757.91
Jorge Sousa Pinto416023.19