Abstract | ||
---|---|---|
This paper presents a system for amorphous program slicing which combines slicing and transformation to achieve thinner slices than are possible using conventional syntax-preserving slicing. The approach involves the validation of the transformation and slicing steps using the Coq proof assistant, thereby guaranteeing the correctness of the amorphous slices produced. The combined application of slicing and transformation is illustrated with a simple case study.Several components of the system implement transformation tactics, such as side-effect removal and dependence reduction transformations which have wider applications than the construction of amorphous slices. |
Year | DOI | Venue |
---|---|---|
2001 | 10.1109/WCRE.2001.957831 | Stuttgart |
Keywords | Field | DocType |
program slicing,program verification,theorem proving,Coq proof assistant,GUSTT,amorphous program slicing,amorphous slicing system,case study,dependence reduction transformations,side-effect removal,syntax-preserving slicing,thinner slices,transformation tactics | Program slicing,Engineering drawing,Computer science,Automated theorem proving,Slicing,Correctness,Theoretical computer science,Amorphous solid,Proof assistant | Conference |
ISSN | ISBN | Citations |
1095-1350 | 0-7695-1303-4 | 15 |
PageRank | References | Authors |
0.72 | 21 | 4 |
Name | Order | Citations | PageRank |
---|---|---|---|
Mark Harman | 1 | 10264 | 389.82 |
Lin Hu | 2 | 15 | 0.72 |
Malcolm Munro | 3 | 877 | 199.56 |
xingyuan zhang | 4 | 106 | 9.80 |