KIT | KIT-Bibliothek | Impressum | Datenschutz

Using Relational Verification for Program Slicing

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

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.

Open Access Logo


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