An Interpolating Sequent Calculus for Quantifier-Free Presburger Arithmetic.
Craig interpolation has become a versatile tool in formal verification, used for instance to generate program assertions that serve as candidates for loop invariants. In this paper, we consider Craig interpolation for quantifier-free Presburger arithmetic (QFPA). Until recently, quantifier eliminati...
| Huvudupphovsmän: | , , , |
|---|---|
| Materialtyp: | Journal article |
| Språk: | English |
| Publicerad: |
2011
|
Search Result 1
An interpolating sequent calculus for quantifier-free Presburger arithmetic
Publicerad 2011
Journal article