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...
Hoofdauteurs: | Kroening, D, Weissenbacher, G |
---|---|
Andere auteurs: | Namjoshi, K |
Formaat: | Book section |
Taal: | English |
Gepubliceerd in: |
2009
|
Onderwerpen: |
Gelijkaardige items
Topics in monitoring and planning for embedded real-time systems
door: Ho, H
Gepubliceerd in: (2015)
door: Ho, H
Gepubliceerd in: (2015)
Gelijkaardige items
-
An Interpolating Decision Procedure for Transitive Relations with Uninterpreted Functions
door: Kroening, D, et al.
Gepubliceerd in: (2010) -
Program analysis with interpolants
door: Weissenbacher, G, et al.
Gepubliceerd in: (2010) -
Repairing strings and trees
door: Riveros Jaeger, C
Gepubliceerd in: (2013) -
Abstract satisfaction
door: Haller, L
Gepubliceerd in: (2013) -
EL-ifying ontologies
door: Carral, D, et al.
Gepubliceerd in: (2014)