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 fragmentin software model checking and provide a preliminary evaluation of its applicability using an interpolation-based program analyser.
- Publication status:
- Published
- Peer review status:
- Peer reviewed
Actions
Access Document
- Files:
-
-
(Preview, pdf, 354.2KB, Terms of use)
-
- Publisher copy:
- 10.1007/978-3-642-19237-1_15
+ EU FP7 STREP MOGENTES
More from this funder
- Funding agency for:
- Weissenbacher, G
- Grant:
- Project ID ICT-216679
+ Semiconductor Research Corporation
More from this funder
- Funding agency for:
- Kroening, D
- Grant:
- 2006-TJ-1539
- 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
- Pages:
- 150-168
- Publication date:
- 2009-01-01
- Edition:
- Accepted Manuscript
- DOI:
- Language:
-
English
- Keywords:
- Subjects:
- UUID:
-
uuid:c46c14d2-aa3b-489e-b9a7-64cb9b0fd1d7
- Local pid:
-
ora:4408
- Deposit date:
-
2010-11-09
Terms of use
- Copyright holder:
- Springer-Verlag Berlin Heidelberg
- Copyright date:
- 2011
- Notes:
- Citation: Kroening, D. & Weissenbacher, G. (2011) An interpolating decision procedure for transitive relations with uninterpreted functions. In: Namjoshi, K., Zeller, A. & Ziv, A. (eds.) 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, pp. 150-168.
If you are the owner of this record, you can report an update to it here: Report update to this record