An interpolating decision procedure for transitive relations with uninterpreted functions

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 ou...

Mô tả đầy đủ

Chi tiết về thư mục
Những tác giả chính: Kroening, D, Weissenbacher, G
Tác giả khác: Namjoshi, K
Định dạng: Book section
Ngôn ngữ:English
Được phát hành: 2009
Những chủ đề:
Miêu tả
Tóm tắt: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.