One of the main challenges in the verification of software systems is
the analysis of programs that make use of the layout of the memory, like
compilers or device drivers. Such programs produce potentially unbounded
and circular data structures that can be modified during the execution
of the program. There are many successful approaches to an analysis of
the memory structure of such programs, like separation logic and shape
analysis.
In this talk, I will present an approach to a more detailed semantic
analysis by combining memory analysis and first-order theorem proving
(FOTP). Although the semantics of a program is usually described by
first-order formulas, it is in itself not a first-order but a minimal
model semantics. Thus the main component of the link of FOTP and program
analysis is an adaption of first-order reasoning to such stronger
semantics. I will show how this adaption can effectively be performed
and present examples of programs that are analyzed using FOTP.