|
Evènement pour le groupe Modélisation et Verification
Date | 2010-02-25 11:30-12:45 |
Titre | Craig Interpolation for Quantifier-Free Presburger Arithmetic |
Résumé | Craig interpolation has become a versatile tool in formal verification,
for instance to generate intermediate assertions for safety
analysis. Interpolants are often determined by annotating the steps
of an unsatisfiability proof with partial interpolants. In this
talk, I consider Craig interpolation for full quantifier-free
Presburger arithmetic (QFPA), for which until recently no efficient
interpolation procedures were known. As one such procedure, I introduce
an interpolating sequent calculus for QFPA and prove it to be sound
and complete. In particular, the complexity of extracting interpolants
from proofs is discussed. Finally, I add support for uninterpreted
predicates to the calculus, thus extending it to important theories such
as arrays and uninterpreted functions.
The talk describes joint work with Angelo Brillout, Daniel Kroening, and
Thomas Wahl.
|
Lieu | Salle 076, LaBRI, Rez-de-chaussée |
Orateur | Philipp Ruemmer |
Email | Philipp.Ruemmer@comlab.ox.ac.uk |
Url | Oxford University, Computing Laboratory, UK |
Aucun document lié à cet événement. RetourRetour à l'index
| |