Room    : CS202J
Date    : 22 February 2007
Time    : 12:15 -- 13:15
Speaker : Jan Tobias Muehlberg
Title   : Towards a Simulation-based Verification of Memory
          Safety Properties for Object Code Programs

Abstract:
While most of us (as long as we are not writing Haskell code) got
used to gaps between our intention and the code we write, we
usually do not think about mismatches between our intention and
the compiler's understanding of the language we are programming
in. However, computers do not execute source-code programs and
one of the greatest hazards in programming still arises from the
use of pointer operations in unsafe programming languages such as
C: If a program dereferences an invalid pointer, the program will
either crash or behave in an undefined way. Unfortunately, these
errors are common, difficult to debug and not covered by today's
software verification systems.

In this talk I will give an overview of my ongoing work on
developing a simulation-based framework for the validation of
safety properties for pointer operations in object code programs.
After defining the properties of interest, I will show how
data-flow analysis and program slicing can be employed in order
to generate program abstractions that preserve interesting memory
safety properties and make efficient program simulation possible.
Running examples are taken from the thrilling domain of Linux
device drivers.