Campus Event Calendar
Event Entry
New for: D2, D3
What and Who
Towards Automated Program Analysis using First-Order Theorem Proving
Matthias Horbach
University of New Mexico
Talk
AG 1, AG 2, AG 3, AG 4, AG 5, SWS, RG1, MMCI
Public Audience
English
Note: We use this to send email in the morning.
Date, Time and Location
Tuesday, 5 July 2011
14:15
60 Minutes
E1 4
024
Saarbrücken
Abstract
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.
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.
Contact
Jennifer Müller
2900
--email hidden
passcode not visible
logged in users only
Jennifer Müller, 07/04/2011 11:49 -- Created document.