Title  : Slicing Object Code
Speaker: Jan Tobias Muehlberg (University of York)
         <muehlber@cs.york.ac.uk>

Slicing is a widely deployed technique for abstracting over program
details that are irrelevant when automatically validating some desired
property of the program.  Unfortunately, most published slicing
algorithms work on source code and are thus not applicable to software
that is only available in object code form.

This talk presents a novel technique for slicing object code that
retains the executability of the resulting slice.  The underlying
approach is based on an intermediate representation that is borrowed
from the binary instrumentation framework Valgrind.  Our slicing
technique lends itself to synthesising models from compiled programs,
in order to reduce execution times for subsequent simulation,
verification and testing.  We have implemented a prototype object-code
slicer as a front-end of a bounded model-checking tool that checks
operating systems software for memory safety.  Our results show that
object-code slicing drastically reduces verification time and speeds-up
code execution when using real Linux device drivers as benchmark.