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

Полное описание

Библиографические подробности
Главные авторы: Kroening, D, Weissenbacher, G
Другие авторы: Namjoshi, K
Формат: Book section
Язык:English
Опубликовано: 2009
Предметы:

Схожие документы