Back to Search

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
Collapse abstract

Publication status:: Published

Actions

Email

Email this record

Send the bibliographic details of this record to your email address.

Your Email
Please enter the email address that the record information will be sent to.

-
Your message (optional)
Please add any additional information to be included within the email.
Cite

Cite this record

APA Style

Brillout, A., Kroening, D., Rümmer, P., & Wahl, T. (2011). An Interpolating Sequent Calculus for Quantifier-Free Presburger Arithmetic. J. Autom. Reasoning, 47(4), 341–367.

MLA Style

Brillout, A., et al. “An Interpolating Sequent Calculus for Quantifier-Free Presburger Arithmetic.” J. Autom. Reasoning, vol. 47, no. 4, 2011, pp. 341–67.

Chicago Style

Brillout, A, D Kroening, P Rümmer, and T Wahl. 2011. “An Interpolating Sequent Calculus for Quantifier-Free Presburger Arithmetic.” J. Autom. Reasoning 47 (4): 341–67.
Tweet
Print

Access Document

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

Authors

+ Brillout, A More by this author

Role:

Author

+ Kroening, D More by this author

Role:

Author

+ Rümmer, P More by this author

Role:

Author

+ Wahl, T More by this author

Role:

Author

Bibliographic Details

Journal:: J. Autom. Reasoning
Volume:: 47
Issue:: 4
Pages:: 341-367
Publication date:: 2011-01-01
DOI:: 10.1007/s10817-011-9237-y
EISSN:: 1573-0670
ISSN:: 0168-7433

Item Description

Language:: English
Keywords:: Presburger arithmetic

Craig interpolation

Sequent calculus
Pubs id:: pubs:327205
UUID:: uuid:c835de4f-0d64-4c87-b805-6949a9b33fc9
Local pid:: pubs:327205
Source identifiers:: 327205
Deposit date:: 2012-12-19

Terms of use

Copyright date:: 2011

Licence:: Terms and Conditions of Use for Oxford University Research Archive

Metrics

Views and Downloads

About views and downloads

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

TO TOP