Home  |  deutsch  |  Legals  |  Data Protection  |  Sitemap  |  KIT

SemSlice: Exploiting Relational Verification for Automatic Program Slicing

Reviewed Paper In Proceedings

Author(s):Bernhard Beckert, Thorsten Bormer, Stephan Gocht, Mihai Herda, Daniel Lentzsch, and Mattias Ulbrich
In:13th International Conference on integrated Formal Methods (iFM 2017)
Publisher:Springer
Series:Lecture Notes in Computer Science
Volume:10510
Year:2017
Pages:312-319
Preprint/PDF:semslice_ifm2017.pdf
DOI:10.1007/978-3-319-66845-1_20

Abstract

We present SemSlice, a tool which automatically produces very precise slices for C routines. 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 close to the minimal number of statements, the program's semantics must be considered. SemSlice is based on automatic relational regression verification, which SemSlice uses to select valid slices from a set of candidate slices. We present several approaches for producing candidates for precise slices. Evaluation shows that regression verification (based on coupling invariant inference) is a powerful tool for semantics-aware slicing: precise slices for typical slicing challenges can be found automatically and fast.

BibTeX

@InProceedings{beckert2017semslice,
  author       = {Bernhard Beckert and Thorsten Bormer and Stephan
                  Gocht and Mihai Herda and Daniel Lentzsch and
                  Mattias Ulbrich},
  title        = {{SemSlice}: Exploiting Relational Verification for
                  Automatic Program Slicing},
  booktitle    = {13th International Conference on integrated Formal
                  Methods ({iFM} 2017)},
  year         = 2017,
  month        = sep,
  place        = {Torino, Italy},
  date         = {September 18-22},
  publisher    = {Springer},
  series       = {Lecture Notes in Computer Science},
  volume       = {10510},
  pages        = {312--319},
  doi          = {10.1007/978-3-319-66845-1_20}
}