Book section icon

Book section

An interpolating decision procedure for transitive relations with uninterpreted functions

Abstract:

We present a proof-generating decision procedure for the quantifier-free fragment of first-order logic with the relations =, !=, >=, and > and argue that this logic, augmented with a set of theory-specific rewriting rules, is adequate for bit-level accurate verification. We describe our decision procedure from an algorithmic point of view and explain how it is possible to efficiently generate Craig interpolants for this logic. Furthermore, we discuss the relevance of the logical fragm...

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

Actions


Access Document


Files:
Publisher copy:
10.1007/978-3-642-19237-1_15

Authors


More by this author
Institution:
University of Oxford
Oxford college:
Magdalen College
Department:
Mathematical,Physical & Life Sciences Division - Computing Laboratory
Role:
Author
More by this author
Institution:
University of Oxford
Oxford college:
Magdalen College
Department:
Mathematical,Physical & Life Sciences Division - Computing Laboratory
Role:
Author

Contributors

Role:
Editor
Role:
Editor
Role:
Editor
More from this funder
Funding agency for:
Georg Weissenbacher
Pages:
150-168
Host title:
Hardware and software: Verification and Testing. 5th International Haifa Verification Conference, HVC 2009, Haifa, Israel, October 19-22, 2009, Revised Selected Papers. Lecture Notes in Computer Science 6405
Publication date:
2009-01-01
DOI:
URN:
uuid:c46c14d2-aa3b-489e-b9a7-64cb9b0fd1d7
Local pid:
ora:4408

Terms of use


Metrics


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