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
|
Θέματα: |
Παρόμοια τεκμήρια
Παρόμοια τεκμήρια
-
An Interpolating Decision Procedure for Transitive Relations with Uninterpreted Functions
ανά: Kroening, D, κ.ά.
Έκδοση: (2010) -
Program analysis with interpolants
ανά: Weissenbacher, G, κ.ά.
Έκδοση: (2010) -
Repairing strings and trees
ανά: Riveros Jaeger, C
Έκδοση: (2013) -
Abstract satisfaction
ανά: Haller, L
Έκδοση: (2013) -
EL-ifying ontologies
ανά: Carral, D, κ.ά.
Έκδοση: (2014)