Being careful about theory combination

Dejan Jovanović, Clark Barrett

Research output: Contribution to journalArticle

Abstract

One of the main shortcomings of traditional methods for combining theories is the complexity of guessing the arrangement of variables shared by the individual theories. This paper presents a reformulation of the Nelson-Oppen method that takes into account explicit equality propagation and can ignore pairs of shared variables that the theories do not care about. We show the correctness of the new approach and present care functions for the theory of uninterpreted functions and the theory of arrays. The effectiveness of the new method is illustrated by experimental results demonstrating a dramatic performance improvement on benchmarks combining arrays and bit-vectors.

Original languageEnglish (US)
Pages (from-to)67-90
Number of pages24
JournalFormal Methods in System Design
Volume42
Issue number1
DOIs
StatePublished - Feb 2013

Fingerprint

Reformulation
Arrangement
Correctness
Equality
Propagation
Benchmark
Experimental Results

Keywords

  • Nelson-Oppen
  • Satisfiability modulo theories
  • Theory combination

ASJC Scopus subject areas

  • Software
  • Hardware and Architecture
  • Theoretical Computer Science

Cite this

Being careful about theory combination. / Jovanović, Dejan; Barrett, Clark.

In: Formal Methods in System Design, Vol. 42, No. 1, 02.2013, p. 67-90.

Research output: Contribution to journalArticle

Jovanović, Dejan ; Barrett, Clark. / Being careful about theory combination. In: Formal Methods in System Design. 2013 ; Vol. 42, No. 1. pp. 67-90.
@article{ba8737bf373f49dcbd81f8067cd546b5,
title = "Being careful about theory combination",
abstract = "One of the main shortcomings of traditional methods for combining theories is the complexity of guessing the arrangement of variables shared by the individual theories. This paper presents a reformulation of the Nelson-Oppen method that takes into account explicit equality propagation and can ignore pairs of shared variables that the theories do not care about. We show the correctness of the new approach and present care functions for the theory of uninterpreted functions and the theory of arrays. The effectiveness of the new method is illustrated by experimental results demonstrating a dramatic performance improvement on benchmarks combining arrays and bit-vectors.",
keywords = "Nelson-Oppen, Satisfiability modulo theories, Theory combination",
author = "Dejan Jovanović and Clark Barrett",
year = "2013",
month = "2",
doi = "10.1007/s10703-012-0159-z",
language = "English (US)",
volume = "42",
pages = "67--90",
journal = "Formal Methods in System Design",
issn = "0925-9856",
publisher = "Springer Netherlands",
number = "1",

}

TY - JOUR

T1 - Being careful about theory combination

AU - Jovanović, Dejan

AU - Barrett, Clark

PY - 2013/2

Y1 - 2013/2

N2 - One of the main shortcomings of traditional methods for combining theories is the complexity of guessing the arrangement of variables shared by the individual theories. This paper presents a reformulation of the Nelson-Oppen method that takes into account explicit equality propagation and can ignore pairs of shared variables that the theories do not care about. We show the correctness of the new approach and present care functions for the theory of uninterpreted functions and the theory of arrays. The effectiveness of the new method is illustrated by experimental results demonstrating a dramatic performance improvement on benchmarks combining arrays and bit-vectors.

AB - One of the main shortcomings of traditional methods for combining theories is the complexity of guessing the arrangement of variables shared by the individual theories. This paper presents a reformulation of the Nelson-Oppen method that takes into account explicit equality propagation and can ignore pairs of shared variables that the theories do not care about. We show the correctness of the new approach and present care functions for the theory of uninterpreted functions and the theory of arrays. The effectiveness of the new method is illustrated by experimental results demonstrating a dramatic performance improvement on benchmarks combining arrays and bit-vectors.

KW - Nelson-Oppen

KW - Satisfiability modulo theories

KW - Theory combination

UR - http://www.scopus.com/inward/record.url?scp=84872400609&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=84872400609&partnerID=8YFLogxK

U2 - 10.1007/s10703-012-0159-z

DO - 10.1007/s10703-012-0159-z

M3 - Article

VL - 42

SP - 67

EP - 90

JO - Formal Methods in System Design

JF - Formal Methods in System Design

SN - 0925-9856

IS - 1

ER -