SemSlice: Exploiting Relational Verification for Automatic Program Slicing

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


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.