Sharing is caring: Combination of theories

Dejan Jovanović, Clark Barrett

Research output: Chapter in Book/Report/Conference proceedingConference 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 languageEnglish (US)
Title of host publicationFrontiers of Combining Systems - 8th International Symposium, FroCoS 2011, Proceedings
Pages195-210
Number of pages16
DOIs
StatePublished - Oct 18 2011
Event8th International Symposium on Frontiers of Combining Systems, FroCoS 2011 - Saarbrucken, Germany
Duration: Oct 5 2011Oct 7 2011

Publication series

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

Other

Other8th International Symposium on Frontiers of Combining Systems, FroCoS 2011
CountryGermany
CitySaarbrucken
Period10/5/1110/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