Journal article icon

Journal article

An interpolating sequent calculus for quantifier-free Presburger arithmetic

Abstract:

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 elimination was the only available interpolation method for this theory, which is, however, known to be potentially costly and inflexible. We introduce an interpolation approach based on a sequent calculus ...

Expand abstract
Publication status:
Published
Peer review status:
Peer reviewed
Version:
Accepted Manuscript

Actions


Access Document


Files:
Publisher copy:
10.1007/s10817-011-9237-y

Authors


Brillout, A More by this author
More by this author
Department:
Oxford, MPLS, Computer Science
Rümmer, P More by this author
Publisher:
Springer Publisher's website
Journal:
Journal of Automated Reasoning Journal website
Volume:
47
Issue:
4
Pages:
341-367
Publication date:
2011-12-01
DOI:
EISSN:
1573-0670
ISSN:
0168-7433
Pubs id:
pubs:327205
URN:
uri:0076e3c3-c779-45fe-95e0-1f390f573e1a
UUID:
uuid:0076e3c3-c779-45fe-95e0-1f390f573e1a
Local pid:
pubs:327205
Keywords:

Terms of use


Metrics



If you are the owner of this record, you can report an update to it here: Report update to this record

TO TOP