Sharing is caring: Combination of theories

Dejan Jovanović; Clark Barrett

doi:10.1007/978-3-642-24364-6_14

Sharing is caring: Combination of theories

Dejan Jovanović, Clark Barrett

Computer Science

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Abstract

One of the main shortcomings of the traditional methods for combining theories is the complexity of guessing the arrangement of the 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 language	English (US)
Title of host publication	Frontiers of Combining Systems - 8th International Symposium, FroCoS 2011, Proceedings
Pages	195-210
Number of pages	16
DOIs	https://doi.org/10.1007/978-3-642-24364-6_14
State	Published - Oct 18 2011
Event	8th International Symposium on Frontiers of Combining Systems, FroCoS 2011 - Saarbrucken, Germany Duration: Oct 5 2011 → Oct 7 2011

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	6989 LNAI
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Other

Other	8th International Symposium on Frontiers of Combining Systems, FroCoS 2011
Country	Germany
City	Saarbrucken
Period	10/5/11 → 10/7/11

Fingerprint

ASJC Scopus subject areas

Theoretical Computer Science
Computer Science(all)

Cite this

Jovanović, D., & Barrett, C. (2011). Sharing is caring: Combination of theories. In Frontiers of Combining Systems - 8th International Symposium, FroCoS 2011, Proceedings (pp. 195-210). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 6989 LNAI). https://doi.org/10.1007/978-3-642-24364-6_14

Sharing is caring : Combination of theories. / Jovanović, Dejan; Barrett, Clark.

Frontiers of Combining Systems - 8th International Symposium, FroCoS 2011, Proceedings. 2011. p. 195-210 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 6989 LNAI).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Jovanović, D & Barrett, C 2011, Sharing is caring: Combination of theories. in Frontiers of Combining Systems - 8th International Symposium, FroCoS 2011, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 6989 LNAI, pp. 195-210, 8th International Symposium on Frontiers of Combining Systems, FroCoS 2011, Saarbrucken, Germany, 10/5/11. https://doi.org/10.1007/978-3-642-24364-6_14

@inproceedings{30e7a4410dfe49cb97a6ed5007616422,

title = "Sharing is caring: Combination of theories",

abstract = "One of the main shortcomings of the traditional methods for combining theories is the complexity of guessing the arrangement of the 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.",

author = "Dejan Jovanovi{\'c} and Clark Barrett",

year = "2011",

month = oct

day = "18",

doi = "10.1007/978-3-642-24364-6_14",

language = "English (US)",

isbn = "9783642243639",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

pages = "195--210",

booktitle = "Frontiers of Combining Systems - 8th International Symposium, FroCoS 2011, Proceedings",

note = "8th International Symposium on Frontiers of Combining Systems, FroCoS 2011 ; Conference date: 05-10-2011 Through 07-10-2011",

}

TY - GEN

T1 - Sharing is caring

T2 - 8th International Symposium on Frontiers of Combining Systems, FroCoS 2011

AU - Jovanović, Dejan

AU - Barrett, Clark

PY - 2011/10/18

Y1 - 2011/10/18

N2 - One of the main shortcomings of the traditional methods for combining theories is the complexity of guessing the arrangement of the 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 the traditional methods for combining theories is the complexity of guessing the arrangement of the 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.

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

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

U2 - 10.1007/978-3-642-24364-6_14

DO - 10.1007/978-3-642-24364-6_14

M3 - Conference contribution

AN - SCOPUS:80054015944

SN - 9783642243639

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 195

EP - 210

BT - Frontiers of Combining Systems - 8th International Symposium, FroCoS 2011, Proceedings

Y2 - 5 October 2011 through 7 October 2011

ER -

Access to Document

10.1007/978-3-642-24364-6_14