Evènement pour le groupe Modélisation et Verification

Date 2010-02-25  11:30-12:45
TitreCraig 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.  
LieuSalle 076, LaBRI, Rez-de-chaussée 
OrateurPhilipp Ruemmer 
UrlOxford University, Computing Laboratory, UK 

Aucun document lié à cet événement.

Retour à l'index