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

Actions


Access Document


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

Authors


More by this author
Institution:
University of Oxford
Division:
MPLS
Department:
Computer Science
Oxford college:
Magdalen College
Role:
Author
More by this author
Institution:
University of Oxford
Division:
MPLS
Department:
Computer Science
Oxford college:
Magdalen College
Role:
Author

Contributors

Role:
Editor
Role:
Editor
Role:
Editor
More from this funder
Funding agency for:
Kroening, D
Grant:
2006-TJ-1539
More from this funder
Funding agency for:
Weissenbacher, G
Grant:
Project ID ICT-216679
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:
Language:
English
Keywords:
Subjects:
UUID:
uuid:c46c14d2-aa3b-489e-b9a7-64cb9b0fd1d7
Local pid:
ora:4408
Deposit date:
2010-11-09

Terms of use


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