@article{NO79,
author= "G. Nelson and D. Oppen",
title={{Simplification by cooperating decision procedures}},
journal="ACM Transactions on Programming Languages and Systems",
volume="1",
number="2",
pages="245-57",
year="1979"}

@article{S84,
author= "R. Shostak",
title={{Deciding combinations of theories}},
journal="Journal of the Association for Computing Machinery",
volume="31",
number="1",
pages="1-12",
year="1984"}

@article{NO80,
author= "G. Nelson and D. Oppen",
title={{Fast decision procedures based on congruence closure}},
journal="Journal of the Association for Computing Machinery",
volume="27",
number="2",
pages="356-64",
year="1980"}

@InProceedings{BarrettBerezin04,
  author =       {Clark Barrett and Sergey Berezin},
  title =        {{CVC} {L}ite: A New Implementation of the Cooperating Validity
 Checker},
  crossref =     {CAV2004},
  url = {http://verify.stanford.edu/PAPERS/cvcl-cav-2004.ps},
}

@proceedings{CAV2004,
  editor    = {Rajeev Alur and Doron A. Peled},
  title     = {Computer Aided Verification, 16th International Conference, CAV
               2004, Boston, Massachusetts, USA, July 13-17, 2004, Proceedings},
  booktitle = {CAV},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  OPTvolume    = {},
  year      = {2004},
  OPTisbn      = {},
}

@InProceedings{BBD03,
  author = 	 {Clark Barrett and Sergey Berezin and David Dill},
  title = 	 {A Proof-Producing Boolean Search Engine},
  booktitle = {{PDPAR}'03 Workshop, Miami, Florida},
  year = 	 {2003},
  month = 	 jul,
  note = 	 {to appear},
  url = {http://verify.stanford.edu/PAPERS/BB-PDPAR-2003.ps},
}


@InProceedings{BerezinGaneshDill03,
  author = 	 {Sergey Berezin and Vijay Ganesh and David L. Dill},
  title = 	 {An Online Proof-Producing Decision Procedure for Mixed-Integer Linear Arithmetic},
  booktitle = 	 {TACAS'03},
  pages = 	 {521--536},
  year = 	 {2003},
  editor = 	 {H. Garavel and J. Hatcliff},
  volume = 	 {2619},
  series = 	 {Lecture Notes in Computer Science},
  OPTaddress = 	 {{W}arsaw {P}oland},
  month = 	 apr,
  publisher = {Springer Verlag},
  url = {http://verify.stanford.edu/PAPERS/BGD03.ps},
}

@inproceedings{SBDL01,
author= "A. Stump and C. Barrett and D. Dill and J. Levitt",
title={{A Decision Procedure for an Extensional Theory of Arrays}},
booktitle="16th IEEE Symposium on Logic in Computer Science",
Publisher="IEEE Computer Society",
pages="29-37",
year = 2001,
url = {http://verify.stanford.edu/PAPERS/LICS-SBDL-2001.pdf},
}


@inproceedings{BDL98,
author = "Clark W. Barrett and David L. Dill and Jeremy R. Levitt",
title = "A Decision Procedure for Bit-Vector Arithmetic",
booktitle="Proceedings of the 35th Design Automation Conference",
Note="San Francisco, CA",
month="June",
year=1998,
url = {http://verify.stanford.edu/PAPERS/BDL98.ps},
}

@phdthesis{B03,
author = "C. Barrett",
title = {{Checking Validity of Quantifier-Free Formulas in Combinations of First
-Order Theories}},
year="2003",
school={Stanford University},
url={http://www.cs.nyu.edu/~barrett/pubs/thesis.ps}
}

@InProceedings{BBSCGD04,
  author =       {Clark Barrett and Sergey Berezin and Igor Shikanian and Marsha
 Chechik and Arie Gurfinkel and David L. Dill},
  title =        {A Practical Approach to Partial Functions in {CVC} {L}ite},

  booktitle = {{PDPAR}'04 Workshop, Cork, Ireland},
  year =         {2004},
  month =        jul,
  url = {http://chicory.stanford.edu/PAPERS/cvcl-pdpar-2004.ps},
}

@inproceedings{ pugh91omega,
    author = "William Pugh",
    title = "The Omega test: a fast and practical integer programming algorithm for dependence analysis",
    booktitle = "Supercomputing",
    pages = "4-13",
    year = "1991",
    url = "citeseer.nj.nec.com/pugh93omega.html" }

@conference{RS01,
author= "H. Ruess and N. Shankar",
title={{Deconstructing Shostak}},
booktitle = "16th IEEE Symposium on Logic in Computer Science",
year = 2001
    URL = {http://www.csl.sri.com/papers/lics01/}
}

@conference{CLS96,
author = "D. Cyrluk and P. Lincoln and N. Shankar",
title = {{On Shostak's Decision Procedure for Combinations of Theories}},
booktitle = "13th International Conference on Computer Aided Deduction",
editor = "M. McRobbie and J. Slaney",
volume =       "1104",
series =       "LNCS",
year =         1996,
publisher = "Springer-Verlag",
pages =        "463-477"
}

@phdthesis{L98,
author = "J. Levitt",
title = {{Formal Verification Techniques for Digital Systems}},
year="1999",
school={Stanford University}}

@TechReport{Gh03,
  author = 	 {S. Ghilardi},
  title = 	 {Reasoners' Cooperation and Quantifier Elimination},
  institution =  {Dipartimento di Scienze dell'Informazione, Universit\`{a} degli Studi di Milano},
  year = 	 {2003},
}

@Misc{simplify,
  OPTkey = 	 {},
  author = 	 {D. Detlefs and G. Nelson and J. Saxe},
  title = 	 {Simplify Theorem Prover},
  howpublished = {\texttt{http://research.compaq.com/SRC/esc/Simplify.html}},
}

@TechReport{GBTD04-TR,
  author = 	 {V. Ganesh and S. Berezin and C. Tinelli and D. L. Dill},
  title = 	 {Combination Results for Many Sorted Theories with Overlapping Signatures},
  institution =  {Stanford University},
  year = 	 {2004},
}

@phdthesis{Zar04b,
   author = "Zarba, Calogero G.",
   title = "The Combination Problem in Automated Reasoning",
   school = "Stanford University",
   year = "2004"
}

@InProceedings{tiwari03,
  author = 	 {Ashish Tiwari},
  title = 	 {Abstraction Based Theorem Proving: An example from the theory of Reals},
  booktitle = {Proceedings of PDPAR'03 workshop at CADE},
  pages = 	 {40--52},
  year = 	 {2003},
  editor = 	 {Silvio Ranise and Cesare Tinelli},
  month = 	 jul,
}

@inproceedings{SBD02,
author= "A. Stump and C. Barrett and D. Dill",
title={{CVC: a Cooperating Validity Checker}},
booktitle="14th International Conference on Computer-Aided Verification",
editors="K. Larsen and E. Brinksma",
year="2002"
url={http://sprout.stanford.edu/PAPERS/CAV-SBD-2002.pdf},
}