KIT | KIT-Bibliothek | Impressum | Datenschutz

Using Relational Verification for Program Slicing

Beckert, Bernhard ORCID iD icon; Bormer, Thorsten; Gocht, Stephan; Herda, Mihai; Lentzsch, Daniel; Ulbrich, Mattias ORCID iD icon

Abstract:

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.


Volltext §
DOI: 10.5445/IR/1000093895
Veröffentlicht am 18.04.2019
Cover der Publikation
Zugehörige Institution(en) am KIT Institut für Theoretische Informatik (ITI)
Publikationstyp Forschungsbericht/Preprint
Publikationsjahr 2019
Sprache Englisch
Identifikator ISSN: 2190-4782
KITopen-ID: 1000093895
Verlag Karlsruher Institut für Technologie (KIT)
Umfang 19 S.
Serie Karlsruhe Reports in Informatics ; 2019,5
Schlagwörter program slicing, relational verification
KIT – Die Forschungsuniversität in der Helmholtz-Gemeinschaft
KITopen Landing Page