Campus Event Calendar
Event Entry
New for: D2, D3
What and Who
Craig interpolation for integer arithmetic, uninterpreted functions, and the theory of arrays
Philipp Ruemmer
Department of Information Technology, Uppsala University
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
Thursday, 30 June 2011
14:15
60 Minutes
E1 4
024
Saarbrücken
Abstract
Craig interpolation has become a versatile tool in formal
verification, in particular for generating intermediate assertions in
safety analysis and model checking. As a result, the development of
efficient interpolation procedures for expressive logical theories has
received a lot of attention over the last years. I will summarise our
recent work on interpolation procedures, for theories for which
previously no efficient procedures were known: quantifier-free
Presburger Arithmetic, in combination with (i) uninterpreted
predicates (QPA+UP), (ii) uninterpreted functions (QPA+UF) and (iii)
extensional arrays (QPA+AR). Since none of the combined theories
can be effectively interpolated without the use of quantifiers, even if
the input formulae are quantifier-free, I will identify fragments
of QPA+UP and QPA+UF with restricted forms of guarded quantification
that are closed under interpolation.
verification, in particular for generating intermediate assertions in
safety analysis and model checking. As a result, the development of
efficient interpolation procedures for expressive logical theories has
received a lot of attention over the last years. I will summarise our
recent work on interpolation procedures, for theories for which
previously no efficient procedures were known: quantifier-free
Presburger Arithmetic, in combination with (i) uninterpreted
predicates (QPA+UP), (ii) uninterpreted functions (QPA+UF) and (iii)
extensional arrays (QPA+AR). Since none of the combined theories
can be effectively interpolated without the use of quantifiers, even if
the input formulae are quantifier-free, I will identify fragments
of QPA+UP and QPA+UF with restricted forms of guarded quantification
that are closed under interpolation.
Contact
Jennifer Müller
2900
--email hidden
passcode not visible
logged in users only
Jennifer Müller, 06/21/2011 12:35 -- Created document.