% coop_dec_procs.bib
% Aaron Stump, 1/9/00
%
% This file contains some references to works about 
% cooperating decision procedures.

@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"
}

@article{armando+03,
author="A. Armando and S. Ranise and M. Rusinowitch",
title={{A Rewriting Approach to Satisfiability Procedeures}},
journal="Information and Computation",
volume=183,
number=2,
month="June",
year=2003,
pages="140--164",
note="Special Issue on the 12th International Conference on Rewriting Techniques and Applications (RTA 2001)"} 

@conference{ARR01,
author = "A. Armando and S. Ranise and M. Rusinowitch",
title = {{Uniform Derivation of Decision Procedures by Superposition}},
booktitle = "Computer Science Logic (CSL01)",
editor = "L. Fribourg",
volume =       "2142",
series =       "LNCS",
year =         2001,
publisher = "Springer-Verlag"
}

@conference{K97,
author = "D. Kapur",
title = {{Shostak's congruence closure as completion}},
booktitle = "8th International Conference on Rewriting Techniques and Applications",
editor = "H. Comon",
year =         1997,
publisher = "Springer-Verlag",
pages =        "23-37"
}

@conference{RS01,
author= "H. Ruess and N. Shankar",
title={{Deconstructing Shostak}},
booktitle = "16th IEEE Symposium on Logic in Computer Science",
year = 2001
}

@inproceedings{fordshankar02,
author="J. Ford and N. Shankar",
title="Formal Verification of a Combination Decision Procedure",
booktitle="18th International Conference on Automated Deduction",
year=2002,
editor="A. Voronkov"}

@conference{BT97,
author = "F. Baader and C. Tinelli",
title = {{A new approach for combining decision procedures for the word problem, and its connection to the Nelson-Oppen combination method}},
booktitle = "14th International Conference on Computer Aided Deduction",
editor = "W. McCune",
series =       "LNCS",
year =         1997,
publisher = "Springer-Verlag",
pages =        "19-33"
}

@conference{TH96,
author = "C. Tinelli and M. Harandi",
title = {{A New Correctness Proof of the Nelson-Oppen Combination Procedure}},
booktitle = "1st International Workshop on Frontiers of Combining Systems (FroCoS'96)",
editor = "F. Baader and K. Schulz",
series = "Applied Logic Series",
volume = "3",
year =   1996,
publisher = "Kluwer",
}

@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{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"}

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

@phdthesis{B98,
author = "N. Bjorner",
title = {{Integrating Decision Procedures for Temporal Verification}},
year="1999",
school={Stanford University}}

@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"}

@techreport{N81,
author = "G. Nelson",
institution = {{Xerox PARC}},
title = {{Techniques for Program Verification}},
number = "CSL-81-10",
month = Jun,
year = "1981"}

@article{DST80,
author= "P. Downey and R. Sethi and R. Tarjan",
title={{Variations on the Common Subexpression Problem}},
journal="Journal of the Association for Computing Machinery",
volume="27",
number="4",
pages="758-71",
year="1980"}

@conference{BT00,
author = "L. Bachmair and A. Tiwari",
title = {{Abstract Congruence Closure and Specializations}},
booktitle = "17th International Conference on Automated Deduction",
Series="LNAI",
Editor="David McAllester",
Publisher="Springer-Verlag",
Volume="1831",
pages="64-78",
year =         2000
}

@inproceedings{Z01,
author = "Zarba, Calogero",
title = "Combining Non-Disjoint Theories",
editor = "Gor{'e}, Rajeev and Leitsch, Alexander and Nipkow, Tobias",
booktitle = "International Joint Conference on Automated Reasoning (Short Papers)",
series = "Technical Report DII 11/01",
pages = "180--189",
organization = "University of Siena, Italy",
year = "2001"
}

% used to be M98

@inproceedings{moeller+98,
  author = 	 "M. M{\"o}ller and H. Rue{\ss}",
  title = 	 {{Solving Bit-Vector Equations}},
  booktitle = 	 "Formal Methods in Computer-Aided Design",
  year = 	 1998,
  pages = 	 "36--48",
}

@phdthesis{M98a,
author = {M. M\"oller},
title = {{Solving Bit-Vector Equations -- a Decision Procedure for Hardware Verification}},
year="1998",
school={University of Ulm}}

@conference{FJOS03,
author = "C. Flanagan and R. Joshi and X. Ou and J. Saxe",
title = {{Theorem Proving using Lazy Proof Explication}},
booktitle = "15th International Conference on Computer-Aided Verification",
editor = "W. Hunt and F. Somenzi",
year =   2003
}

@inproceedings{BD04,
author="C. Barrett and J. Donham",
title={{Combining SAT Methods with Non-Clausal Decision Heuristics}},
booktitle={{Pragmatics of Decision Procedures in Automated Reasoning}},
editor="S. Ranise and C. Tinelli",
year=2004}

@inproceedings{kozen77,
author="D. Kozen",
title={{Complexity of Finitely Presented Algebras}},
booktitle="In Proceedings of the 9th Annual ACM Symposium on Theory of Computing",
pages="164--177", 
year=1977}

@InProceedings{BaaGT-IJCAR-04,
  author =	 {F. Baader and S. Ghilardi and C. Tinelli},
  title =	 {A New Combination Procedure for the Word Problem
                  that Generalizes Fusion Decidability Results in
                  Modal Logics},
  booktitle =	 {Proceedings of the 2nd International Joint
                  Conference on Automated Reasoning},
  year =	 2004,
  editor =	 {D.~Basin and M.~Rusinowitch},
  series =	 {Lecture Notes in Artificial Intelligence},
  publisher =	 {Springer-Verlag}
}

@inproceedings{nieuwenhuis+05,
author="R. Nieuwenhuis and A. Oliveras",
title={{Proof-producing Congruence Closure}},
booktitle="16th International Conference on Rewriting Techniques and Applications",
editor="J. Giesl",
pages="453--468",
publisher="Springer",
year=2005}

@inproceedings{nieuwenhuis+04,
author="R. Nieuwenhuis and A. Oliveras",
title={{Union-Find and Congruence Closure Algorithms that Produce Proofs}},
booktitle="2nd International Workshop on Pragmatics of Decision Procedures in Automated Reasoning",
editor="S. Ranise and C. Tinelli",
note="(short paper)",
year=2004}

@article{demoura+04,
	TITLE = {{Justifying Equality}},
	AUTHOR = {L. de Moura and H. Rue{\ss} and N. Shankar},
editor="W. Ahrendt and P. Baumgartner and H. de Nivelle and S. Ranise and C. Tinelli",
volume=125,
number=3,
pages="69--85",
journal = "Electronic Notes in Theoretical Computer Science",
note={Appeared at the 2nd International Workshop on Pragmatics of Decision
Procedures in Automated Reasoning (2004)},
year=2005}

@inproceedings{seshia+04,
author="S. Seshia and R. Bryant",
title={{Deciding Quantifier-Free Presburger Formulas Using Parameterized Solution Bounds}},
booktitle={Logic in Computer Science},
year=2004,
publisher="IEEE"}

@inproceedings{Barrett+04,
author = {Clark Barrett and Sergey Berezin},
title = {{CVC L}ite: A New Implementation of the Cooperating Validity Checker},
booktitle = {Proceedings of the 16th International Conference on Computer Aided Verification},
editor = "R. Alur",
year = 2004
}

@inproceedings{audemard+02,
title={{A SAT Based Approach for Solving Formulas over Boolean and Linear Mathematical Propositions}},
author = "G. Audemard and P. Bertoli and A. Cimatti and A. Kornilowicz and R. Sebastiani",
booktitle="18th International Conference on Automated Deduction",
editor="A. Voronkov",
year=2002}

@inproceedings{armando+04,
author="A. Armando and C. Castellini and E. Giunchiglia and M. Maratea",
title={{A SAT-based Decision Procedure for the Boolean Combination of Difference Constraints}},
booktitle="7th International Conference on Theory and Applications of Satisfiability Testing",
editor="H. Hoos and D. Mitchell",
year=2004}

@inproceedings{bachmair+02,
author = "L. Bachmair and A. Tiwari",
title = {{Abstract Congruence Closure and Specializations}},
booktitle="17th International Conference on Automated Deduction",
year=2000,
editor="D. McAllester"}

@inproceedings{YorshMusuvathi05,
author = "G. Yorsh and M. Musuvathi",
title="A Combination Method for Generating Interpolants",
booktitle="20th Internation Conference on Automated Deduction",
editor="R. Nieuwenhuis",
year=2005}

@article{detlefs2005stp,
  title={{Simplify: a theorem prover for program checking}},
  author={Detlefs, D. and Nelson, G. and Saxe, J.B.},
  journal={Journal of the ACM (JACM)},
  volume={52},
  number={3},
  pages={365--473},
  year={2005},
  publisher={ACM Press New York, NY, USA}
}

@inproceedings{Moura+07,
  author    = {L. de Moura and
               N. Bj{\o}rner},
  title     = {{Efficient E-Matching for SMT Solvers}},
  booktitle = {Conference on Automated Deduction},
  year      = {2007},
  pages     = {183-198},
  editor    = "F. Pfenning"
}

@article{Nieuwenhuis+07,
  author    = {R. Nieuwenhuis and A. Oliveras},
  title     = {{Fast Congruence Closure and Extensions}},
  journal   = {Information and Computation},
  volume    = {205},
  number    = {4},
  year      = {2007},
  pages     = {557-580}
}

@inproceedings{BT07,
  author    = "C. Barrett and C. Tinelli",
  title     = "{CVC3}",
  booktitle = "Proceedings of the $19^{th}$ International Conference on Computer Aided Verification (CAV '07)",
  publisher = "Springer-Verlag",
  editor    = "W. Damm and H. Hermanns",
  pages     = "298--302",
  year      = 2007
}

@Misc{SMT-LIB,
  author =       {S. Ranise and C. Tinelli},
  title =        {{The SMT-LIB Standard, Version 1.2}},
  note =         {Available from the "Documents" section of http://combination.cs.uiowa.edu/smtlib},
  year =         2006
}

@inproceedings{moskal08,
author = "M. Moskal",
title={{Rocket-Fast Proof Checking for SMT Solvers}},
booktitle="Tools and Algorithms for the Construction
and Analysis of Systems",
editor="C. Ramakrishnan and J. Rehof",
year = 2008}

@InProceedings{Fontaine+08,
  author =       "Pascal Fontaine and Jean-Yves Marion and Stephan Merz
                 and Leonor Prensa Nieto and Alwen Tiu",
  title =        "Expressiveness + Automation + Soundness: Towards
                 Combining {SMT} Solvers and Interactive Proof
                 Assistants",
  booktitle =    tacas,
  editor =       "Holger Hermanns and Jens Palsberg",
  year =         "2006",
  pages =        "167--181",
  series =       "Lecture Notes in Computer Science",
  publisher =    "Springer-Verlag",
  volume =       "3920",
}
