Beyond quantifier-free interpolation in extensions of presburger arithmetic
Craig interpolation has emerged as an effective means of generating candidate program invariants. We present interpolation procedures for the theories of Presburger arithmetic combined with (i) uninterpreted predicates (QPA+UP), (ii) uninterpreted functions (QPA+UF) and (iii) extensional arrays (QPA...
| المؤلفون الرئيسيون: | , , , |
|---|---|
| مؤلفون آخرون: | |
| التنسيق: | Conference item |
| منشور في: |
Springer
2011
|