Campus Event Calendar
Event Entry
New for: D1, D2, D3, D4, D5
What and Who
INTERPOLATION FOR DATA STRUCTURES - Talk within RG1 meeting -
Calogero Zarba
Fachrichtung Informatik - Saarbrücken
Talk
AG 1, AG 2, AG 3, AG 4, AG 5, SWS
AG Audience
English
Note: We use this to send email in the morning.
Date, Time and Location
Wednesday, 11 October 2006
11:00
-- Not specified --
E1 4
Rotunda 6th floor
Saarbrücken
Abstract
Interpolation based automatic abstraction is a powerful and robust
technique for the automated analysis of hardware and software systems.
In this talk we present a general algorithm to construct interpolants
for any recursively enumerable theory. In particular, efficient
procedures to construct interpolants for the theories of arrays, sets,
and multisets are discussed using the reduction approach for obtaining
decision procedures for complex data structures. The approach taken
is that of reducing the theories of such data structures to the
theories of equality and linear arithmetic for which efficient
interpolating decision procedures exist. This enables interpolation
based techniques to be applied to programs that manipulate these data
technique for the automated analysis of hardware and software systems.
In this talk we present a general algorithm to construct interpolants
for any recursively enumerable theory. In particular, efficient
procedures to construct interpolants for the theories of arrays, sets,
and multisets are discussed using the reduction approach for obtaining
decision procedures for complex data structures. The approach taken
is that of reducing the theories of such data structures to the
theories of equality and linear arithmetic for which efficient
interpolating decision procedures exist. This enables interpolation
based techniques to be applied to programs that manipulate these data
Contact
Roxane Wetzel
900
--email hidden
passcode not visible
logged in users only
Roxane Wetzel, 10/11/2006 14:46 -- Created document.