BibTeX records: Cesare Tinelli

download as .bib file

@article{DBLP:journals/lmcs/BansalBRT18,
  author    = {Kshitij Bansal and
               Clark Barrett and
               Andrew Reynolds and
               Cesare Tinelli},
  title     = {Reasoning with Finite Sets and Cardinality Constraints in {SMT}},
  journal   = {Logical Methods in Computer Science},
  volume    = {14},
  number    = {4},
  year      = {2018},
  url       = {https://doi.org/10.23638/LMCS-14(4:12)2018},
  doi       = {10.23638/LMCS-14(4:12)2018},
  timestamp = {Wed, 21 Nov 2018 00:00:00 +0100},
  biburl    = {https://dblp.org/rec/bib/journals/lmcs/BansalBRT18},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cade/ReynoldsVBTB18,
  author    = {Andrew Reynolds and
               Arjun Viswanathan and
               Haniel Barbosa and
               Cesare Tinelli and
               Clark Barrett},
  title     = {Datatypes with Shared Selectors},
  booktitle = {Automated Reasoning - 9th International Joint Conference, {IJCAR}
               2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford,
               UK, July 14-17, 2018, Proceedings},
  pages     = {591--608},
  year      = {2018},
  crossref  = {DBLP:conf/cade/2018},
  url       = {https://doi.org/10.1007/978-3-319-94205-6\_39},
  doi       = {10.1007/978-3-319-94205-6\_39},
  timestamp = {Mon, 09 Jul 2018 12:59:13 +0200},
  biburl    = {https://dblp.org/rec/bib/conf/cade/ReynoldsVBTB18},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cav/NiemetzPRBT18,
  author    = {Aina Niemetz and
               Mathias Preiner and
               Andrew Reynolds and
               Clark Barrett and
               Cesare Tinelli},
  title     = {Solving Quantified Bit-Vectors Using Invertibility Conditions},
  booktitle = {Computer Aided Verification - 30th International Conference, {CAV}
               2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford,
               UK, July 14-17, 2018, Proceedings, Part {II}},
  pages     = {236--255},
  year      = {2018},
  crossref  = {DBLP:conf/cav/2018-2},
  url       = {https://doi.org/10.1007/978-3-319-96142-2\_16},
  doi       = {10.1007/978-3-319-96142-2\_16},
  timestamp = {Wed, 03 Oct 2018 01:00:00 +0200},
  biburl    = {https://dblp.org/rec/bib/conf/cav/NiemetzPRBT18},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@incollection{DBLP:reference/mc/BarrettT18,
  author    = {Clark Barrett and
               Cesare Tinelli},
  title     = {Satisfiability Modulo Theories},
  booktitle = {Handbook of Model Checking.},
  pages     = {305--343},
  year      = {2018},
  crossref  = {DBLP:reference/mc/2018},
  url       = {https://doi.org/10.1007/978-3-319-10575-8\_11},
  doi       = {10.1007/978-3-319-10575-8\_11},
  timestamp = {Tue, 29 May 2018 12:30:27 +0200},
  biburl    = {https://dblp.org/rec/bib/reference/mc/BarrettT18},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/corr/abs-1804-05025,
  author    = {Aina Niemetz and
               Mathias Preiner and
               Andrew Reynolds and
               Clark Barrett and
               Cesare Tinelli},
  title     = {On Solving Quantified Bit-Vectors using Invertibility Conditions},
  journal   = {CoRR},
  volume    = {abs/1804.05025},
  year      = {2018},
  url       = {http://arxiv.org/abs/1804.05025},
  archivePrefix = {arXiv},
  eprint    = {1804.05025},
  timestamp = {Mon, 13 Aug 2018 01:00:00 +0200},
  biburl    = {https://dblp.org/rec/bib/journals/corr/abs-1804-05025},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/corr/abs-1806-08775,
  author    = {Clark Barrett and
               Haniel Barbosa and
               Martin Brain and
               Duligur Ibeling and
               Tim King and
               Paul Meng and
               Aina Niemetz and
               Andres N{\"{o}}tzli and
               Mathias Preiner and
               Andrew Reynolds and
               Cesare Tinelli},
  title     = {{CVC4} at the {SMT} Competition 2018},
  journal   = {CoRR},
  volume    = {abs/1806.08775},
  year      = {2018},
  url       = {http://arxiv.org/abs/1806.08775},
  archivePrefix = {arXiv},
  eprint    = {1806.08775},
  timestamp = {Mon, 13 Aug 2018 01:00:00 +0200},
  biburl    = {https://dblp.org/rec/bib/journals/corr/abs-1806-08775},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/acta/BaierT17,
  author    = {Christel Baier and
               Cesare Tinelli},
  title     = {Special issue of the 21st International Conference on Tools and Algorithms
               for the Construction and Analysis of Systems {(TACAS} 2015)},
  journal   = {Acta Inf.},
  volume    = {54},
  number    = {8},
  pages     = {727--728},
  year      = {2017},
  url       = {https://doi.org/10.1007/s00236-017-0298-1},
  doi       = {10.1007/s00236-017-0298-1},
  timestamp = {Tue, 26 Jun 2018 01:00:00 +0200},
  biburl    = {https://dblp.org/rec/bib/journals/acta/BaierT17},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/sttt/BaierT17,
  author    = {Christel Baier and
               Cesare Tinelli},
  title     = {Some advances in tools and algorithms for the construction and analysis
               of systems},
  journal   = {{STTT}},
  volume    = {19},
  number    = {6},
  pages     = {649--652},
  year      = {2017},
  url       = {https://doi.org/10.1007/s10009-017-0471-4},
  doi       = {10.1007/s10009-017-0471-4},
  timestamp = {Mon, 16 Oct 2017 01:00:00 +0200},
  biburl    = {https://dblp.org/rec/bib/journals/sttt/BaierT17},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/tplp/ReynoldsTB17,
  author    = {Andrew Reynolds and
               Cesare Tinelli and
               Clark Barrett},
  title     = {Constraint solving for finite model finding in {SMT} solvers},
  journal   = {{TPLP}},
  volume    = {17},
  number    = {4},
  pages     = {516--558},
  year      = {2017},
  url       = {https://doi.org/10.1017/S1471068417000175},
  doi       = {10.1017/S1471068417000175},
  timestamp = {Wed, 30 Aug 2017 01:00:00 +0200},
  biburl    = {https://dblp.org/rec/bib/journals/tplp/ReynoldsTB17},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cade/MengRTB17,
  author    = {Baoluo Meng and
               Andrew Reynolds and
               Cesare Tinelli and
               Clark W. Barrett},
  title     = {Relational Constraint Solving in {SMT}},
  booktitle = {Automated Deduction - {CADE} 26 - 26th International Conference on
               Automated Deduction, Gothenburg, Sweden, August 6-11, 2017, Proceedings},
  pages     = {148--165},
  year      = {2017},
  crossref  = {DBLP:conf/cade/2017},
  url       = {https://doi.org/10.1007/978-3-319-63046-5\_10},
  doi       = {10.1007/978-3-319-63046-5\_10},
  timestamp = {Wed, 12 Jul 2017 10:06:41 +0200},
  biburl    = {https://dblp.org/rec/bib/conf/cade/MengRTB17},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cav/EkiciMTKKRB17,
  author    = {Burak Ekici and
               Alain Mebsout and
               Cesare Tinelli and
               Chantal Keller and
               Guy Katz and
               Andrew Reynolds and
               Clark W. Barrett},
  title     = {SMTCoq: {A} Plug-In for Integrating {SMT} Solvers into Coq},
  booktitle = {Computer Aided Verification - 29th International Conference, {CAV}
               2017, Heidelberg, Germany, July 24-28, 2017, Proceedings, Part {II}},
  pages     = {126--133},
  year      = {2017},
  crossref  = {DBLP:conf/cav/2017-2},
  url       = {https://doi.org/10.1007/978-3-319-63390-9\_7},
  doi       = {10.1007/978-3-319-63390-9\_7},
  timestamp = {Fri, 14 Jul 2017 13:04:29 +0200},
  biburl    = {https://dblp.org/rec/bib/conf/cav/EkiciMTKKRB17},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cav/ReynoldsWBBLT17,
  author    = {Andrew Reynolds and
               Maverick Woo and
               Clark Barrett and
               David Brumley and
               Tianyi Liang and
               Cesare Tinelli},
  title     = {Scaling Up {DPLL(T)} String Solvers Using Context-Dependent Simplification},
  booktitle = {Computer Aided Verification - 29th International Conference, {CAV}
               2017, Heidelberg, Germany, July 24-28, 2017, Proceedings, Part {II}},
  pages     = {453--474},
  year      = {2017},
  crossref  = {DBLP:conf/cav/2017-2},
  url       = {https://doi.org/10.1007/978-3-319-63390-9\_24},
  doi       = {10.1007/978-3-319-63390-9\_24},
  timestamp = {Fri, 14 Jul 2017 13:04:29 +0200},
  biburl    = {https://dblp.org/rec/bib/conf/cav/ReynoldsWBBLT17},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/frocos/ReynoldsTJB17,
  author    = {Andrew Reynolds and
               Cesare Tinelli and
               Dejan Jovanovic and
               Clark Barrett},
  title     = {Designing Theory Solvers with Extensions},
  booktitle = {Frontiers of Combining Systems - 11th International Symposium, FroCoS
               2017, Bras{\'{\i}}lia, Brazil, September 27-29, 2017, Proceedings},
  pages     = {22--40},
  year      = {2017},
  crossref  = {DBLP:conf/frocos/2017},
  url       = {https://doi.org/10.1007/978-3-319-66167-4\_2},
  doi       = {10.1007/978-3-319-66167-4\_2},
  timestamp = {Tue, 05 Sep 2017 14:29:33 +0200},
  biburl    = {https://dblp.org/rec/bib/conf/frocos/ReynoldsTJB17},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/nfm/WagnerMTCS17,
  author    = {Lucas G. Wagner and
               Alain Mebsout and
               Cesare Tinelli and
               Darren D. Cofer and
               Konrad Slind},
  title     = {Qualification of a Model Checker for Avionics Software Verification},
  booktitle = {{NASA} Formal Methods - 9th International Symposium, {NFM} 2017, Moffett
               Field, CA, USA, May 16-18, 2017, Proceedings},
  pages     = {404--419},
  year      = {2017},
  crossref  = {DBLP:conf/nfm/2017},
  url       = {https://doi.org/10.1007/978-3-319-57288-8\_29},
  doi       = {10.1007/978-3-319-57288-8\_29},
  timestamp = {Thu, 25 May 2017 01:00:00 +0200},
  biburl    = {https://dblp.org/rec/bib/conf/nfm/WagnerMTCS17},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:journals/corr/abs-1711-10641,
  author    = {Andrew Reynolds and
               Cesare Tinelli},
  title     = {SyGuS Techniques in the Core of an {SMT} Solver},
  booktitle = {Proceedings Sixth Workshop on Synthesis, SYNT@CAV 2017, Heidelberg,
               Germany, 22nd July 2017.},
  pages     = {81--96},
  year      = {2017},
  crossref  = {DBLP:journals/corr/abs-1711-10224},
  url       = {https://doi.org/10.4204/EPTCS.260.8},
  doi       = {10.4204/EPTCS.260.8},
  timestamp = {Wed, 12 Sep 2018 01:00:00 +0200},
  biburl    = {https://dblp.org/rec/bib/journals/corr/abs-1711-10641},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/corr/BansalBRT17,
  author    = {Kshitij Bansal and
               Clark W. Barrett and
               Andrew Reynolds and
               Cesare Tinelli},
  title     = {A New Decision Procedure for Finite Sets and Cardinality Constraints
               in {SMT}},
  journal   = {CoRR},
  volume    = {abs/1702.06259},
  year      = {2017},
  url       = {http://arxiv.org/abs/1702.06259},
  archivePrefix = {arXiv},
  eprint    = {1702.06259},
  timestamp = {Mon, 13 Aug 2018 01:00:00 +0200},
  biburl    = {https://dblp.org/rec/bib/journals/corr/BansalBRT17},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/corr/ReynoldsTB17,
  author    = {Andrew Reynolds and
               Cesare Tinelli and
               Clark W. Barrett},
  title     = {Constraint Solving for Finite Model Finding in {SMT} Solvers},
  journal   = {CoRR},
  volume    = {abs/1706.00096},
  year      = {2017},
  url       = {http://arxiv.org/abs/1706.00096},
  archivePrefix = {arXiv},
  eprint    = {1706.00096},
  timestamp = {Mon, 13 Aug 2018 01:00:00 +0200},
  biburl    = {https://dblp.org/rec/bib/journals/corr/ReynoldsTB17},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/dagstuhl-reports/BlanchetteFST17,
  author    = {Jasmin Christian Blanchette and
               Carsten Fuhs and
               Viorica Sofronie{-}Stokkermans and
               Cesare Tinelli},
  title     = {Deduction Beyond First-Order Logic (Dagstuhl Seminar 17371)},
  journal   = {Dagstuhl Reports},
  volume    = {7},
  number    = {9},
  pages     = {26--46},
  year      = {2017},
  url       = {https://doi.org/10.4230/DagRep.7.9.26},
  doi       = {10.4230/DagRep.7.9.26},
  timestamp = {Mon, 12 Mar 2018 00:00:00 +0100},
  biburl    = {https://dblp.org/rec/bib/journals/dagstuhl-reports/BlanchetteFST17},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/fmsd/LiangRTTBD16,
  author    = {Tianyi Liang and
               Andrew Reynolds and
               Nestan Tsiskaridze and
               Cesare Tinelli and
               Clark Barrett and
               Morgan Deters},
  title     = {An efficient {SMT} solver for string constraints},
  journal   = {Formal Methods in System Design},
  volume    = {48},
  number    = {3},
  pages     = {206--234},
  year      = {2016},
  url       = {https://doi.org/10.1007/s10703-016-0247-6},
  doi       = {10.1007/s10703-016-0247-6},
  timestamp = {Thu, 15 Jun 2017 01:00:00 +0200},
  biburl    = {https://dblp.org/rec/bib/journals/fmsd/LiangRTTBD16},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cade/BansalRBT16,
  author    = {Kshitij Bansal and
               Andrew Reynolds and
               Clark W. Barrett and
               Cesare Tinelli},
  title     = {A New Decision Procedure for Finite Sets and Cardinality Constraints
               in {SMT}},
  booktitle = {Automated Reasoning - 8th International Joint Conference, {IJCAR}
               2016, Coimbra, Portugal, June 27 - July 2, 2016, Proceedings},
  pages     = {82--98},
  year      = {2016},
  crossref  = {DBLP:conf/cade/2016},
  url       = {https://doi.org/10.1007/978-3-319-40229-1\_7},
  doi       = {10.1007/978-3-319-40229-1\_7},
  timestamp = {Thu, 15 Jun 2017 01:00:00 +0200},
  biburl    = {https://dblp.org/rec/bib/conf/cade/BansalRBT16},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cade/ReynoldsBCT16,
  author    = {Andrew Reynolds and
               Jasmin Christian Blanchette and
               Simon Cruanes and
               Cesare Tinelli},
  title     = {Model Finding for Recursive Functions in {SMT}},
  booktitle = {Automated Reasoning - 8th International Joint Conference, {IJCAR}
               2016, Coimbra, Portugal, June 27 - July 2, 2016, Proceedings},
  pages     = {133--151},
  year      = {2016},
  crossref  = {DBLP:conf/cade/2016},
  url       = {https://doi.org/10.1007/978-3-319-40229-1\_10},
  doi       = {10.1007/978-3-319-40229-1\_10},
  timestamp = {Thu, 15 Jun 2017 01:00:00 +0200},
  biburl    = {https://dblp.org/rec/bib/conf/cade/ReynoldsBCT16},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cav/ChampionMST16,
  author    = {Adrien Champion and
               Alain Mebsout and
               Christoph Sticksel and
               Cesare Tinelli},
  title     = {The Kind 2 Model Checker},
  booktitle = {Computer Aided Verification - 28th International Conference, {CAV}
               2016, Toronto, ON, Canada, July 17-23, 2016, Proceedings, Part {II}},
  pages     = {510--517},
  year      = {2016},
  crossref  = {DBLP:conf/cav/2016-2},
  url       = {https://doi.org/10.1007/978-3-319-41540-6\_29},
  doi       = {10.1007/978-3-319-41540-6\_29},
  timestamp = {Thu, 15 Jun 2017 01:00:00 +0200},
  biburl    = {https://dblp.org/rec/bib/conf/cav/ChampionMST16},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/fmcad/KatzBTRH16,
  author    = {Guy Katz and
               Clark W. Barrett and
               Cesare Tinelli and
               Andrew Reynolds and
               Liana Hadarean},
  title     = {Lazy proofs for DPLL(T)-based {SMT} solvers},
  booktitle = {2016 Formal Methods in Computer-Aided Design, {FMCAD} 2016, Mountain
               View, CA, USA, October 3-6, 2016},
  pages     = {93--100},
  year      = {2016},
  crossref  = {DBLP:conf/fmcad/2016},
  url       = {https://doi.org/10.1109/FMCAD.2016.7886666},
  doi       = {10.1109/FMCAD.2016.7886666},
  timestamp = {Wed, 17 May 2017 01:00:00 +0200},
  biburl    = {https://dblp.org/rec/bib/conf/fmcad/KatzBTRH16},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/fmcad/MebsoutT16,
  author    = {Alain Mebsout and
               Cesare Tinelli},
  title     = {Proof certificates for SMT-based model checkers for infinite-state
               systems},
  booktitle = {2016 Formal Methods in Computer-Aided Design, {FMCAD} 2016, Mountain
               View, CA, USA, October 3-6, 2016},
  pages     = {117--124},
  year      = {2016},
  crossref  = {DBLP:conf/fmcad/2016},
  url       = {https://doi.org/10.1109/FMCAD.2016.7886669},
  doi       = {10.1109/FMCAD.2016.7886669},
  timestamp = {Wed, 17 May 2017 01:00:00 +0200},
  biburl    = {https://dblp.org/rec/bib/conf/fmcad/MebsoutT16},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/hotsos/BarrettTDLRT16,
  author    = {Clark W. Barrett and
               Cesare Tinelli and
               Morgan Deters and
               Tianyi Liang and
               Andrew Reynolds and
               Nestan Tsiskaridze},
  title     = {Efficient solving of string constraints for security analysis},
  booktitle = {Proceedings of the Symposium and Bootcamp on the Science of Security,
               Pittsburgh, PA, USA, April 19-21, 2016},
  pages     = {4--6},
  year      = {2016},
  crossref  = {DBLP:conf/hotsos/2016},
  url       = {https://doi.org/10.1145/2898375.2898393},
  doi       = {10.1145/2898375.2898393},
  timestamp = {Tue, 06 Nov 2018 00:00:00 +0100},
  biburl    = {https://dblp.org/rec/bib/conf/hotsos/BarrettTDLRT16},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/sefm/ChampionGKT16,
  author    = {Adrien Champion and
               Arie Gurfinkel and
               Temesghen Kahsai and
               Cesare Tinelli},
  title     = {CoCoSpec: {A} Mode-Aware Contract Language for Reactive Systems},
  booktitle = {Software Engineering and Formal Methods - 14th International Conference,
               {SEFM} 2016, Held as Part of {STAF} 2016, Vienna, Austria, July 4-8,
               2016, Proceedings},
  pages     = {347--366},
  year      = {2016},
  crossref  = {DBLP:conf/sefm/2016},
  url       = {https://doi.org/10.1007/978-3-319-41591-8\_24},
  doi       = {10.1007/978-3-319-41591-8\_24},
  timestamp = {Thu, 15 Jun 2017 01:00:00 +0200},
  biburl    = {https://dblp.org/rec/bib/conf/sefm/ChampionGKT16},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:journals/corr/EkiciKKMRT16,
  author    = {Burak Ekici and
               Guy Katz and
               Chantal Keller and
               Alain Mebsout and
               Andrew J. Reynolds and
               Cesare Tinelli},
  title     = {Extending SMTCoq, a Certified Checker for {SMT} (Extended Abstract)},
  booktitle = {Proceedings First International Workshop on Hammers for Type Theories,
               HaTT@IJCAR 2016, Coimbra, Portugal, July 1, 2016.},
  pages     = {21--29},
  year      = {2016},
  crossref  = {DBLP:journals/corr/BlanchetteK16},
  url       = {https://doi.org/10.4204/EPTCS.210.5},
  doi       = {10.4204/EPTCS.210.5},
  timestamp = {Wed, 12 Sep 2018 01:05:14 +0200},
  biburl    = {https://dblp.org/rec/bib/journals/corr/EkiciKKMRT16},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/arith/BrainTRW15,
  author    = {Martin Brain and
               Cesare Tinelli and
               Philipp R{\"{u}}mmer and
               Thomas Wahl},
  title     = {An Automatable Formal Semantics for {IEEE-754} Floating-Point Arithmetic},
  booktitle = {22nd {IEEE} Symposium on Computer Arithmetic, {ARITH} 2015, Lyon,
               France, June 22-24, 2015},
  pages     = {160--167},
  year      = {2015},
  crossref  = {DBLP:conf/arith/2015},
  url       = {https://doi.org/10.1109/ARITH.2015.26},
  doi       = {10.1109/ARITH.2015.26},
  timestamp = {Thu, 15 Jun 2017 01:00:00 +0200},
  biburl    = {https://dblp.org/rec/bib/conf/arith/BrainTRW15},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cav/ReynoldsDKTB15,
  author    = {Andrew Reynolds and
               Morgan Deters and
               Viktor Kuncak and
               Cesare Tinelli and
               Clark W. Barrett},
  title     = {Counterexample-Guided Quantifier Instantiation for Synthesis in {SMT}},
  booktitle = {Computer Aided Verification - 27th International Conference, {CAV}
               2015, San Francisco, CA, USA, July 18-24, 2015, Proceedings, Part
               {II}},
  pages     = {198--216},
  year      = {2015},
  crossref  = {DBLP:conf/cav/2015},
  url       = {https://doi.org/10.1007/978-3-319-21668-3\_12},
  doi       = {10.1007/978-3-319-21668-3\_12},
  timestamp = {Thu, 15 Jun 2017 01:00:00 +0200},
  biburl    = {https://dblp.org/rec/bib/conf/cav/ReynoldsDKTB15},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/frocos/LiangTRTB15,
  author    = {Tianyi Liang and
               Nestan Tsiskaridze and
               Andrew Reynolds and
               Cesare Tinelli and
               Clark Barrett},
  title     = {A Decision Procedure for Regular Membership and Length Constraints
               over Unbounded Strings},
  booktitle = {Frontiers of Combining Systems - 10th International Symposium, FroCoS
               2015, Wroclaw, Poland, September 21-24, 2015. Proceedings},
  pages     = {135--150},
  year      = {2015},
  crossref  = {DBLP:conf/frocos/2015},
  url       = {https://doi.org/10.1007/978-3-319-24246-0\_9},
  doi       = {10.1007/978-3-319-24246-0\_9},
  timestamp = {Thu, 15 Jun 2017 21:43:48 +0200},
  biburl    = {https://dblp.org/rec/bib/conf/frocos/LiangTRTB15},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/lpar/HadareanBRTD15,
  author    = {Liana Hadarean and
               Clark W. Barrett and
               Andrew Reynolds and
               Cesare Tinelli and
               Morgan Deters},
  title     = {Fine Grained {SMT} Proofs for the Theory of Fixed-Width Bit-Vectors},
  booktitle = {Logic for Programming, Artificial Intelligence, and Reasoning - 20th
               International Conference, {LPAR-20} 2015, Suva, Fiji, November 24-28,
               2015, Proceedings},
  pages     = {340--355},
  year      = {2015},
  crossref  = {DBLP:conf/lpar/2015},
  url       = {https://doi.org/10.1007/978-3-662-48899-7\_24},
  doi       = {10.1007/978-3-662-48899-7\_24},
  timestamp = {Fri, 02 Nov 2018 09:44:58 +0100},
  biburl    = {https://dblp.org/rec/bib/conf/lpar/HadareanBRTD15},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@proceedings{DBLP:conf/tacas/2015,
  editor    = {Christel Baier and
               Cesare Tinelli},
  title     = {Tools and Algorithms for the Construction and Analysis of Systems
               - 21st International Conference, {TACAS} 2015, Held as Part of the
               European Joint Conferences on Theory and Practice of Software, {ETAPS}
               2015, London, UK, April 11-18, 2015. Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {9035},
  publisher = {Springer},
  year      = {2015},
  url       = {https://doi.org/10.1007/978-3-662-46681-0},
  doi       = {10.1007/978-3-662-46681-0},
  isbn      = {978-3-662-46680-3},
  timestamp = {Thu, 15 Jun 2017 01:00:00 +0200},
  biburl    = {https://dblp.org/rec/bib/conf/tacas/2015},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/corr/ReynoldsDKBT15,
  author    = {Andrew Reynolds and
               Morgan Deters and
               Viktor Kuncak and
               Clark W. Barrett and
               Cesare Tinelli},
  title     = {On Counterexample Guided Quantifier Instantiation for Synthesis in
               {CVC4}},
  journal   = {CoRR},
  volume    = {abs/1502.04464},
  year      = {2015},
  url       = {http://arxiv.org/abs/1502.04464},
  archivePrefix = {arXiv},
  eprint    = {1502.04464},
  timestamp = {Mon, 13 Aug 2018 01:00:00 +0200},
  biburl    = {https://dblp.org/rec/bib/journals/corr/ReynoldsDKBT15},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cade/StumpST14,
  author    = {Aaron Stump and
               Geoff Sutcliffe and
               Cesare Tinelli},
  title     = {StarExec: {A} Cross-Community Infrastructure for Logic Solving},
  booktitle = {Automated Reasoning - 7th International Joint Conference, {IJCAR}
               2014, Held as Part of the Vienna Summer of Logic, {VSL} 2014, Vienna,
               Austria, July 19-22, 2014. Proceedings},
  pages     = {367--373},
  year      = {2014},
  crossref  = {DBLP:conf/cade/2014},
  url       = {https://doi.org/10.1007/978-3-319-08587-6\_28},
  doi       = {10.1007/978-3-319-08587-6\_28},
  timestamp = {Thu, 15 Jun 2017 01:00:00 +0200},
  biburl    = {https://dblp.org/rec/bib/conf/cade/StumpST14},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cav/LiangRTBD14,
  author    = {Tianyi Liang and
               Andrew Reynolds and
               Cesare Tinelli and
               Clark Barrett and
               Morgan Deters},
  title     = {A {DPLL(T)} Theory Solver for a Theory of Strings and Regular Expressions},
  booktitle = {Computer Aided Verification - 26th International Conference, {CAV}
               2014, Held as Part of the Vienna Summer of Logic, {VSL} 2014, Vienna,
               Austria, July 18-22, 2014. Proceedings},
  pages     = {646--662},
  year      = {2014},
  crossref  = {DBLP:conf/cav/2014},
  url       = {https://doi.org/10.1007/978-3-319-08867-9\_43},
  doi       = {10.1007/978-3-319-08867-9\_43},
  timestamp = {Wed, 03 Oct 2018 01:00:00 +0200},
  biburl    = {https://dblp.org/rec/bib/conf/cav/LiangRTBD14},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cav/HadareanBJBT14,
  author    = {Liana Hadarean and
               Kshitij Bansal and
               Dejan Jovanovic and
               Clark Barrett and
               Cesare Tinelli},
  title     = {A Tale of Two Solvers: Eager and Lazy Approaches to Bit-Vectors},
  booktitle = {Computer Aided Verification - 26th International Conference, {CAV}
               2014, Held as Part of the Vienna Summer of Logic, {VSL} 2014, Vienna,
               Austria, July 18-22, 2014. Proceedings},
  pages     = {680--695},
  year      = {2014},
  crossref  = {DBLP:conf/cav/2014},
  url       = {https://doi.org/10.1007/978-3-319-08867-9\_45},
  doi       = {10.1007/978-3-319-08867-9\_45},
  timestamp = {Wed, 03 Oct 2018 01:00:00 +0200},
  biburl    = {https://dblp.org/rec/bib/conf/cav/HadareanBJBT14},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/fmcad/DetersR0BT14,
  author    = {Morgan Deters and
               Andrew Reynolds and
               Tim King and
               Clark W. Barrett and
               Cesare Tinelli},
  title     = {A tour of {CVC4:} How it works, and how to use it},
  booktitle = {Formal Methods in Computer-Aided Design, {FMCAD} 2014, Lausanne, Switzerland,
               October 21-24, 2014},
  pages     = {7},
  year      = {2014},
  crossref  = {DBLP:conf/fmcad/2014},
  url       = {https://doi.org/10.1109/FMCAD.2014.6987586},
  doi       = {10.1109/FMCAD.2014.6987586},
  timestamp = {Thu, 15 Jun 2017 01:00:00 +0200},
  biburl    = {https://dblp.org/rec/bib/conf/fmcad/DetersR0BT14},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/fmcad/0001BT14,
  author    = {Tim King and
               Clark W. Barrett and
               Cesare Tinelli},
  title     = {Leveraging linear and mixed integer programming for {SMT}},
  booktitle = {Formal Methods in Computer-Aided Design, {FMCAD} 2014, Lausanne, Switzerland,
               October 21-24, 2014},
  pages     = {139--146},
  year      = {2014},
  crossref  = {DBLP:conf/fmcad/2014},
  url       = {https://doi.org/10.1109/FMCAD.2014.6987606},
  doi       = {10.1109/FMCAD.2014.6987606},
  timestamp = {Wed, 14 Nov 2018 00:00:00 +0100},
  biburl    = {https://dblp.org/rec/bib/conf/fmcad/0001BT14},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/fmcad/ReynoldsTM14,
  author    = {Andrew Reynolds and
               Cesare Tinelli and
               Leonardo Mendon{\c{c}}a de Moura},
  title     = {Finding conflicting instances of quantified formulas in {SMT}},
  booktitle = {Formal Methods in Computer-Aided Design, {FMCAD} 2014, Lausanne, Switzerland,
               October 21-24, 2014},
  pages     = {195--202},
  year      = {2014},
  crossref  = {DBLP:conf/fmcad/2014},
  url       = {https://doi.org/10.1109/FMCAD.2014.6987613},
  doi       = {10.1109/FMCAD.2014.6987613},
  timestamp = {Thu, 15 Jun 2017 01:00:00 +0200},
  biburl    = {https://dblp.org/rec/bib/conf/fmcad/ReynoldsTM14},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/smt/0001BT14,
  author    = {Tim King and
               Clark Barrett and
               Cesare Tinelli},
  title     = {Leveraging Linear and Mixed Integer Programming for {SMT}},
  booktitle = {Proceedings of the 12th International Workshop on Satisfiability Modulo
               Theories, {SMT} 2014, affiliated with the 26th International Conference
               on Computer Aided Verification {(CAV} 2014), the 7th International
               Joint Conference on Automated Reasoning {(IJCAR} 2014), and the 17th
               International Conference on Theory and Applications of Satisfiability
               Testing {(SAT} 2014), Vienna, Austria, July 17-18, 2014.},
  pages     = {65},
  year      = {2014},
  crossref  = {DBLP:conf/smt/2014},
  url       = {http://ceur-ws.org/Vol-1163/paper-10.pdf},
  timestamp = {Mon, 30 May 2016 16:28:37 +0200},
  biburl    = {https://dblp.org/rec/bib/conf/smt/0001BT14},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/fmsd/StumpORHT13,
  author    = {Aaron Stump and
               Duckki Oe and
               Andrew Reynolds and
               Liana Hadarean and
               Cesare Tinelli},
  title     = {{SMT} proof checking using a logical framework},
  journal   = {Formal Methods in System Design},
  volume    = {42},
  number    = {1},
  pages     = {91--118},
  year      = {2013},
  url       = {https://doi.org/10.1007/s10703-012-0163-3},
  doi       = {10.1007/s10703-012-0163-3},
  timestamp = {Thu, 15 Jun 2017 01:00:00 +0200},
  biburl    = {https://dblp.org/rec/bib/journals/fmsd/StumpORHT13},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cade/ReynoldsTGKDB13,
  author    = {Andrew Reynolds and
               Cesare Tinelli and
               Amit Goel and
               Sava Krstic and
               Morgan Deters and
               Clark Barrett},
  title     = {Quantifier Instantiation Techniques for Finite Model Finding in {SMT}},
  booktitle = {Automated Deduction - {CADE-24} - 24th International Conference on
               Automated Deduction, Lake Placid, NY, USA, June 9-14, 2013. Proceedings},
  pages     = {377--391},
  year      = {2013},
  crossref  = {DBLP:conf/cade/2013},
  url       = {https://doi.org/10.1007/978-3-642-38574-2\_26},
  doi       = {10.1007/978-3-642-38574-2\_26},
  timestamp = {Thu, 15 Jun 2017 01:00:00 +0200},
  biburl    = {https://dblp.org/rec/bib/conf/cade/ReynoldsTGKDB13},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cav/ReynoldsTGK13,
  author    = {Andrew Reynolds and
               Cesare Tinelli and
               Amit Goel and
               Sava Krstic},
  title     = {Finite Model Finding in {SMT}},
  booktitle = {Computer Aided Verification - 25th International Conference, {CAV}
               2013, Saint Petersburg, Russia, July 13-19, 2013. Proceedings},
  pages     = {640--655},
  year      = {2013},
  crossref  = {DBLP:conf/cav/2013},
  url       = {https://doi.org/10.1007/978-3-642-39799-8\_42},
  doi       = {10.1007/978-3-642-39799-8\_42},
  timestamp = {Wed, 03 Oct 2018 01:00:00 +0200},
  biburl    = {https://dblp.org/rec/bib/conf/cav/ReynoldsTGK13},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/nfm/GarocheKT13,
  author    = {Pierre{-}Lo{\"{\i}}c Garoche and
               Temesghen Kahsai and
               Cesare Tinelli},
  title     = {Incremental Invariant Generation Using Logic-Based Automatic Abstract
               Transformers},
  booktitle = {{NASA} Formal Methods, 5th International Symposium, {NFM} 2013, Moffett
               Field, CA, USA, May 14-16, 2013. Proceedings},
  pages     = {139--154},
  year      = {2013},
  crossref  = {DBLP:conf/nfm/2013},
  url       = {https://doi.org/10.1007/978-3-642-38088-4\_10},
  doi       = {10.1007/978-3-642-38088-4\_10},
  timestamp = {Thu, 15 Jun 2017 01:00:00 +0200},
  biburl    = {https://dblp.org/rec/bib/conf/nfm/GarocheKT13},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/corr/abs-1111-5652,
  author    = {Alexander Fuchs and
               Amit Goel and
               Jim Grundy and
               Sava Krstic and
               Cesare Tinelli},
  title     = {Ground interpolation for the theory of equality},
  journal   = {Logical Methods in Computer Science},
  volume    = {8},
  number    = {1},
  year      = {2012},
  url       = {https://doi.org/10.2168/LMCS-8(1:6)2012},
  doi       = {10.2168/LMCS-8(1:6)2012},
  timestamp = {Mon, 13 Aug 2018 01:00:00 +0200},
  biburl    = {https://dblp.org/rec/bib/journals/corr/abs-1111-5652},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/jsc/BaumgartnerPT12,
  author    = {Peter Baumgartner and
               Bj{\"{o}}rn Pelzer and
               Cesare Tinelli},
  title     = {Model Evolution with equality - Revised and implemented},
  journal   = {J. Symb. Comput.},
  volume    = {47},
  number    = {9},
  pages     = {1011--1045},
  year      = {2012},
  url       = {https://doi.org/10.1016/j.jsc.2011.12.031},
  doi       = {10.1016/j.jsc.2011.12.031},
  timestamp = {Sun, 12 Nov 2017 00:00:00 +0100},
  biburl    = {https://dblp.org/rec/bib/journals/jsc/BaumgartnerPT12},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cade/StumpST12,
  author    = {Aaron Stump and
               Geoff Sutcliffe and
               Cesare Tinelli},
  title     = {Introducing StarExec: a Cross-Community Infrastructure for Logic Solving},
  booktitle = {Proceedings of the 1st International Workshop on Comparative Empirical
               Evaluation of Reasoning Systems, Manchester, United Kingdom, June
               30, 2012},
  pages     = {2},
  year      = {2012},
  crossref  = {DBLP:conf/cade/2012compare},
  url       = {http://ceur-ws.org/Vol-873/papers/inv\_1.pdf},
  timestamp = {Mon, 30 May 2016 16:43:12 +0200},
  biburl    = {https://dblp.org/rec/bib/conf/cade/StumpST12},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cade/LiangT12,
  author    = {Tianyi Liang and
               Cesare Tinelli},
  title     = {Exploiting parallelism in the {ME} calculus},
  booktitle = {Third Workshop on Practical Aspects of Automated Reasoning, PAAR-2012,
               Manchester, UK, June 30 - July 1, 2012},
  pages     = {96--108},
  year      = {2012},
  crossref  = {DBLP:conf/cade/2012paar},
  url       = {http://www.easychair.org/publications/paper/145182},
  timestamp = {Tue, 25 Jul 2017 01:00:00 +0200},
  biburl    = {https://dblp.org/rec/bib/conf/cade/LiangT12},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/nfm/Tinelli12,
  author    = {Cesare Tinelli},
  title     = {SMT-Based Model Checking},
  booktitle = {{NASA} Formal Methods - 4th International Symposium, {NFM} 2012, Norfolk,
               VA, USA, April 3-5, 2012. Proceedings},
  pages     = {1},
  year      = {2012},
  crossref  = {DBLP:conf/nfm/2012},
  url       = {https://doi.org/10.1007/978-3-642-28891-3\_1},
  doi       = {10.1007/978-3-642-28891-3\_1},
  timestamp = {Thu, 15 Jun 2017 01:00:00 +0200},
  biburl    = {https://dblp.org/rec/bib/conf/nfm/Tinelli12},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/nfm/KahsaiGTW12,
  author    = {Temesghen Kahsai and
               Pierre{-}Lo{\"{\i}}c Garoche and
               Cesare Tinelli and
               Mike Whalen},
  title     = {Incremental Verification with Mode Variable Invariants in State Machines},
  booktitle = {{NASA} Formal Methods - 4th International Symposium, {NFM} 2012, Norfolk,
               VA, USA, April 3-5, 2012. Proceedings},
  pages     = {388--402},
  year      = {2012},
  crossref  = {DBLP:conf/nfm/2012},
  url       = {https://doi.org/10.1007/978-3-642-28891-3\_35},
  doi       = {10.1007/978-3-642-28891-3\_35},
  timestamp = {Thu, 15 Jun 2017 01:00:00 +0200},
  biburl    = {https://dblp.org/rec/bib/conf/nfm/KahsaiGTW12},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@proceedings{DBLP:conf/cade/2010emsqms,
  editor    = {Aaron Stump and
               Geoff Sutcliffe and
               Cesare Tinelli},
  title     = {Workshop on Evaluation Methods for Solvers, and Quality Metrics for
               Solutions, {EMSQMS} 2010, Edinburgh, UK, July 20, 2010},
  series    = {EPiC Series in Computing},
  volume    = {6},
  publisher = {EasyChair},
  year      = {2012},
  url       = {http://www.easychair.org/publications/?page=249381807},
  timestamp = {Thu, 16 Jun 2016 01:00:00 +0200},
  biburl    = {https://dblp.org/rec/bib/conf/cade/2010emsqms},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/corr/abs-1205-3758,
  author    = {Pierre{-}Lo{\"{\i}}c Garoche and
               Temesghen Kahsai and
               Cesare Tinelli},
  title     = {Invariant stream generators using automatic abstract transformers
               based on a decidable logic},
  journal   = {CoRR},
  volume    = {abs/1205.3758},
  year      = {2012},
  url       = {http://arxiv.org/abs/1205.3758},
  archivePrefix = {arXiv},
  eprint    = {1205.3758},
  timestamp = {Mon, 13 Aug 2018 01:00:00 +0200},
  biburl    = {https://dblp.org/rec/bib/journals/corr/abs-1205-3758},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cade/BaumgartnerT11,
  author    = {Peter Baumgartner and
               Cesare Tinelli},
  title     = {Model Evolution with Equality Modulo Built-in Theories},
  booktitle = {Automated Deduction - {CADE-23} - 23rd International Conference on
               Automated Deduction, Wroclaw, Poland, July 31 - August 5, 2011. Proceedings},
  pages     = {85--100},
  year      = {2011},
  crossref  = {DBLP:conf/cade/2011},
  url       = {https://doi.org/10.1007/978-3-642-22438-6\_9},
  doi       = {10.1007/978-3-642-22438-6\_9},
  timestamp = {Sun, 12 Nov 2017 00:00:00 +0100},
  biburl    = {https://dblp.org/rec/bib/conf/cade/BaumgartnerT11},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cav/BarrettCDHJKRT11,
  author    = {Clark Barrett and
               Christopher L. Conway and
               Morgan Deters and
               Liana Hadarean and
               Dejan Jovanovic and
               Tim King and
               Andrew Reynolds and
               Cesare Tinelli},
  title     = {{CVC4}},
  booktitle = {Computer Aided Verification - 23rd International Conference, {CAV}
               2011, Snowbird, UT, USA, July 14-20, 2011. Proceedings},
  pages     = {171--177},
  year      = {2011},
  crossref  = {DBLP:conf/cav/2011},
  url       = {https://doi.org/10.1007/978-3-642-22110-1\_14},
  doi       = {10.1007/978-3-642-22110-1\_14},
  timestamp = {Wed, 03 Oct 2018 01:00:00 +0200},
  biburl    = {https://dblp.org/rec/bib/conf/cav/BarrettCDHJKRT11},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/nfm/KahsaiGT11,
  author    = {Temesghen Kahsai and
               Yeting Ge and
               Cesare Tinelli},
  title     = {Instantiation-Based Invariant Discovery},
  booktitle = {{NASA} Formal Methods - Third International Symposium, {NFM} 2011,
               Pasadena, CA, USA, April 18-20, 2011. Proceedings},
  pages     = {192--206},
  year      = {2011},
  crossref  = {DBLP:conf/nfm/2011},
  url       = {https://doi.org/10.1007/978-3-642-20398-5\_15},
  doi       = {10.1007/978-3-642-20398-5\_15},
  timestamp = {Thu, 15 Jun 2017 01:00:00 +0200},
  biburl    = {https://dblp.org/rec/bib/conf/nfm/KahsaiGT11},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:journals/corr/abs-1111-0372,
  author    = {Temesghen Kahsai and
               Cesare Tinelli},
  title     = {PKind: {A} parallel k-induction based model checker},
  booktitle = {Proceedings 10th International Workshop on Parallel and Distributed
               Methods in verifiCation, {PDMC} 2011, Snowbird, Utah, USA, July 14,
               2011.},
  pages     = {55--62},
  year      = {2011},
  crossref  = {DBLP:journals/corr/abs-1111-0064},
  url       = {https://doi.org/10.4204/EPTCS.72.6},
  doi       = {10.4204/EPTCS.72.6},
  timestamp = {Wed, 12 Sep 2018 01:05:14 +0200},
  biburl    = {https://dblp.org/rec/bib/journals/corr/abs-1111-0372},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@proceedings{DBLP:conf/frocos/2011,
  editor    = {Cesare Tinelli and
               Viorica Sofronie{-}Stokkermans},
  title     = {Frontiers of Combining Systems, 8th International Symposium, FroCoS
               2011, Saarbr{\"{u}}cken, Germany, October 5-7, 2011. Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {6989},
  publisher = {Springer},
  year      = {2011},
  url       = {https://doi.org/10.1007/978-3-642-24364-6},
  doi       = {10.1007/978-3-642-24364-6},
  isbn      = {978-3-642-24363-9},
  timestamp = {Thu, 15 Jun 2017 01:00:00 +0200},
  biburl    = {https://dblp.org/rec/bib/conf/frocos/2011},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/hvc/BarrettMRST10,
  author    = {Clark Barrett and
               Leonardo Mendon{\c{c}}a de Moura and
               Silvio Ranise and
               Aaron Stump and
               Cesare Tinelli},
  title     = {The {SMT-LIB} Initiative and the Rise of {SMT} - {(HVC} 2010 Award
               Talk)},
  booktitle = {Hardware and Software: Verification and Testing - 6th International
               Haifa Verification Conference, {HVC} 2010, Haifa, Israel, October
               4-7, 2010. Revised Selected Papers},
  pages     = {3},
  year      = {2010},
  crossref  = {DBLP:conf/hvc/2010},
  url       = {https://doi.org/10.1007/978-3-642-19583-9\_2},
  doi       = {10.1007/978-3-642-19583-9\_2},
  timestamp = {Tue, 26 Jun 2018 01:00:00 +0200},
  biburl    = {https://dblp.org/rec/bib/conf/hvc/BarrettMRST10},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/wollic/Tinelli10,
  author    = {Cesare Tinelli},
  title     = {Foundations of Satisfiability Modulo Theories},
  booktitle = {Logic, Language, Information and Computation, 17th International Workshop,
               WoLLIC 2010, Brasilia, Brazil, July 6-9, 2010. Proceedings},
  pages     = {58},
  year      = {2010},
  crossref  = {DBLP:conf/wollic/2010},
  url       = {https://doi.org/10.1007/978-3-642-13824-9\_6},
  doi       = {10.1007/978-3-642-13824-9\_6},
  timestamp = {Wed, 14 Nov 2018 10:55:35 +0100},
  biburl    = {https://dblp.org/rec/bib/conf/wollic/Tinelli10},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/amai/GeBT09,
  author    = {Yeting Ge and
               Clark W. Barrett and
               Cesare Tinelli},
  title     = {Solving quantified verification conditions using satisfiability modulo
               theories},
  journal   = {Ann. Math. Artif. Intell.},
  volume    = {55},
  number    = {1-2},
  pages     = {101--122},
  year      = {2009},
  url       = {https://doi.org/10.1007/s10472-009-9153-6},
  doi       = {10.1007/s10472-009-9153-6},
  timestamp = {Thu, 15 Jun 2017 01:00:00 +0200},
  biburl    = {https://dblp.org/rec/bib/journals/amai/GeBT09},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/japll/BaumgartnerFNT09,
  author    = {Peter Baumgartner and
               Alexander Fuchs and
               Hans de Nivelle and
               Cesare Tinelli},
  title     = {Computing finite models by reduction to function-free clause logic},
  journal   = {J. Applied Logic},
  volume    = {7},
  number    = {1},
  pages     = {58--74},
  year      = {2009},
  url       = {https://doi.org/10.1016/j.jal.2007.07.005},
  doi       = {10.1016/j.jal.2007.07.005},
  timestamp = {Sun, 12 Nov 2017 00:00:00 +0100},
  biburl    = {https://dblp.org/rec/bib/journals/japll/BaumgartnerFNT09},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cade/GoelKT09,
  author    = {Amit Goel and
               Sava Krstic and
               Cesare Tinelli},
  title     = {Ground Interpolation for Combined Theories},
  booktitle = {Automated Deduction - CADE-22, 22nd International Conference on Automated
               Deduction, Montreal, Canada, August 2-7, 2009. Proceedings},
  pages     = {183--198},
  year      = {2009},
  crossref  = {DBLP:conf/cade/2009},
  url       = {https://doi.org/10.1007/978-3-642-02959-2\_16},
  doi       = {10.1007/978-3-642-02959-2\_16},
  timestamp = {Thu, 15 Jun 2017 01:00:00 +0200},
  biburl    = {https://dblp.org/rec/bib/conf/cade/GoelKT09},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/tacas/FuchsGGKT09,
  author    = {Alexander Fuchs and
               Amit Goel and
               Jim Grundy and
               Sava Krstic and
               Cesare Tinelli},
  title     = {Ground Interpolation for the Theory of Equality},
  booktitle = {Tools and Algorithms for the Construction and Analysis of Systems,
               15th International Conference, {TACAS} 2009, Held as Part of the Joint
               European Conferences on Theory and Practice of Software, {ETAPS} 2009,
               York, UK, March 22-29, 2009. Proceedings},
  pages     = {413--427},
  year      = {2009},
  crossref  = {DBLP:conf/tacas/2009},
  url       = {https://doi.org/10.1007/978-3-642-00768-2\_34},
  doi       = {10.1007/978-3-642-00768-2\_34},
  timestamp = {Tue, 26 Jun 2018 01:00:00 +0200},
  biburl    = {https://dblp.org/rec/bib/conf/tacas/FuchsGGKT09},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@incollection{DBLP:series/faia/BarrettSST09,
  author    = {Clark W. Barrett and
               Roberto Sebastiani and
               Sanjit A. Seshia and
               Cesare Tinelli},
  title     = {Satisfiability Modulo Theories},
  booktitle = {Handbook of Satisfiability},
  pages     = {825--885},
  year      = {2009},
  crossref  = {DBLP:series/faia/2009-185},
  url       = {https://doi.org/10.3233/978-1-58603-929-5-825},
  doi       = {10.3233/978-1-58603-929-5-825},
  timestamp = {Tue, 16 May 2017 01:00:00 +0200},
  biburl    = {https://dblp.org/rec/bib/series/faia/BarrettSST09},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/ai/BaumgartnerT08,
  author    = {Peter Baumgartner and
               Cesare Tinelli},
  title     = {The model evolution calculus as a first-order {DPLL} method},
  journal   = {Artif. Intell.},
  volume    = {172},
  number    = {4-5},
  pages     = {591--632},
  year      = {2008},
  url       = {https://doi.org/10.1016/j.artint.2007.09.005},
  doi       = {10.1016/j.artint.2007.09.005},
  timestamp = {Sun, 12 Nov 2017 00:00:00 +0100},
  biburl    = {https://dblp.org/rec/bib/journals/ai/BaumgartnerT08},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/fmcad/HagenT08,
  author    = {George Hagen and
               Cesare Tinelli},
  title     = {Scaling Up the Formal Verification of Lustre Programs with SMT-Based
               Techniques},
  booktitle = {Formal Methods in Computer-Aided Design, {FMCAD} 2008, Portland, Oregon,
               USA, 17-20 November 2008},
  pages     = {1--9},
  year      = {2008},
  crossref  = {DBLP:conf/fmcad/2008},
  url       = {https://doi.org/10.1109/FMCAD.2008.ECP.19},
  doi       = {10.1109/FMCAD.2008.ECP.19},
  timestamp = {Thu, 15 Jun 2017 01:00:00 +0200},
  biburl    = {https://dblp.org/rec/bib/conf/fmcad/HagenT08},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/lpar/BaumgartnerFT08,
  author    = {Peter Baumgartner and
               Alexander Fuchs and
               Cesare Tinelli},
  title     = {{(LIA)} - Model Evolution with Linear Integer Arithmetic Constraints},
  booktitle = {Logic for Programming, Artificial Intelligence, and Reasoning, 15th
               International Conference, {LPAR} 2008, Doha, Qatar, November 22-27,
               2008. Proceedings},
  pages     = {258--273},
  year      = {2008},
  crossref  = {DBLP:conf/lpar/2008},
  url       = {https://doi.org/10.1007/978-3-540-89439-1\_19},
  doi       = {10.1007/978-3-540-89439-1\_19},
  timestamp = {Sun, 12 Nov 2017 00:00:00 +0100},
  biburl    = {https://dblp.org/rec/bib/conf/lpar/BaumgartnerFT08},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/entcs/BarrettST07,
  author    = {Clark Barrett and
               Igor Shikanian and
               Cesare Tinelli},
  title     = {An Abstract Decision Procedure for Satisfiability in the Theory of
               Recursive Data Types},
  journal   = {Electr. Notes Theor. Comput. Sci.},
  volume    = {174},
  number    = {8},
  pages     = {23--37},
  year      = {2007},
  url       = {https://doi.org/10.1016/j.entcs.2006.11.037},
  doi       = {10.1016/j.entcs.2006.11.037},
  timestamp = {Wed, 14 Jun 2017 01:00:00 +0200},
  biburl    = {https://dblp.org/rec/bib/journals/entcs/BarrettST07},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/jsat/BarrettST07,
  author    = {Clark Barrett and
               Igor Shikanian and
               Cesare Tinelli},
  title     = {An Abstract Decision Procedure for a Theory of Inductive Data Types},
  journal   = {{JSAT}},
  volume    = {3},
  number    = {1-2},
  pages     = {21--46},
  year      = {2007},
  url       = {https://satassociation.org/jsat/index.php/jsat/article/view/33},
  timestamp = {Tue, 17 Apr 2018 01:00:00 +0200},
  biburl    = {https://dblp.org/rec/bib/journals/jsat/BarrettST07},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cade/GeBT07,
  author    = {Yeting Ge and
               Clark Barrett and
               Cesare Tinelli},
  title     = {Solving Quantified Verification Conditions Using Satisfiability Modulo
               Theories},
  booktitle = {Automated Deduction - CADE-21, 21st International Conference on Automated
               Deduction, Bremen, Germany, July 17-20, 2007, Proceedings},
  pages     = {167--182},
  year      = {2007},
  crossref  = {DBLP:conf/cade/2007},
  url       = {https://doi.org/10.1007/978-3-540-73595-3\_12},
  doi       = {10.1007/978-3-540-73595-3\_12},
  timestamp = {Thu, 15 Jun 2017 01:00:00 +0200},
  biburl    = {https://dblp.org/rec/bib/conf/cade/GeBT07},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cade/Tinelli07,
  author    = {Cesare Tinelli},
  title     = {Trends and Challenges in Satisfiability Modulo Theories},
  booktitle = {Proceedings of 4th International Verification Workshop in connection
               with CADE-21, Bremen, Germany, July 15-16, 2007},
  year      = {2007},
  crossref  = {DBLP:conf/cade/2007verify},
  url       = {http://ceur-ws.org/Vol-259/paper03.pdf},
  timestamp = {Mon, 30 May 2016 16:57:34 +0200},
  biburl    = {https://dblp.org/rec/bib/conf/cade/Tinelli07},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cav/BarrettT07,
  author    = {Clark Barrett and
               Cesare Tinelli},
  title     = {{CVC3}},
  booktitle = {Computer Aided Verification, 19th International Conference, {CAV}
               2007, Berlin, Germany, July 3-7, 2007, Proceedings},
  pages     = {298--302},
  year      = {2007},
  crossref  = {DBLP:conf/cav/2007},
  url       = {https://doi.org/10.1007/978-3-540-73368-3\_34},
  doi       = {10.1007/978-3-540-73368-3\_34},
  timestamp = {Wed, 03 Oct 2018 01:00:00 +0200},
  biburl    = {https://dblp.org/rec/bib/conf/cav/BarrettT07},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/tableaux/Tinelli07,
  author    = {Cesare Tinelli},
  title     = {An Abstract Framework for Satisfiability Modulo Theories},
  booktitle = {Automated Reasoning with Analytic Tableaux and Related Methods, 16th
               International Conference, {TABLEAUX} 2007, Aix en Provence, France,
               July 3-6, 2007, Proceedings},
  pages     = {10},
  year      = {2007},
  crossref  = {DBLP:conf/tableaux/2007},
  url       = {https://doi.org/10.1007/978-3-540-73099-6\_3},
  doi       = {10.1007/978-3-540-73099-6\_3},
  timestamp = {Thu, 15 Jun 2017 01:00:00 +0200},
  biburl    = {https://dblp.org/rec/bib/conf/tableaux/Tinelli07},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/tacas/KrsticGGT07,
  author    = {Sava Krstic and
               Amit Goel and
               Jim Grundy and
               Cesare Tinelli},
  title     = {Combined Satisfiability Modulo Parametric Theories},
  booktitle = {Tools and Algorithms for the Construction and Analysis of Systems,
               13th International Conference, {TACAS} 2007, Held as Part of the Joint
               European Conferences on Theory and Practice of Software, {ETAPS} 2007
               Braga, Portugal, March 24 - April 1, 2007, Proceedings},
  pages     = {602--617},
  year      = {2007},
  crossref  = {DBLP:conf/tacas/2007},
  url       = {https://doi.org/10.1007/978-3-540-71209-1\_47},
  doi       = {10.1007/978-3-540-71209-1\_47},
  timestamp = {Tue, 26 Jun 2018 01:00:00 +0200},
  biburl    = {https://dblp.org/rec/bib/conf/tacas/KrsticGGT07},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/expert/BeckertHHSGRTBR06,
  author    = {Bernhard Beckert and
               Tony Hoare and
               Reiner H{\"{a}}hnle and
               Douglas R. Smith and
               Cordell Green and
               Silvio Ranise and
               Cesare Tinelli and
               Thomas Ball and
               Sriram K. Rajamani},
  title     = {Intelligent Systems and Formal Methods in Software Engineering},
  journal   = {{IEEE} Intelligent Systems},
  volume    = {21},
  number    = {6},
  pages     = {71--81},
  year      = {2006},
  url       = {https://doi.org/10.1109/MIS.2006.117},
  doi       = {10.1109/MIS.2006.117},
  timestamp = {Fri, 30 Nov 2018 00:00:00 +0100},
  biburl    = {https://dblp.org/rec/bib/journals/expert/BeckertHHSGRTBR06},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/iandc/BaaderGT06,
  author    = {Franz Baader and
               Silvio Ghilardi and
               Cesare Tinelli},
  title     = {A new combination procedure for the word problem that generalizes
               fusion decidability results in modal logics},
  journal   = {Inf. Comput.},
  volume    = {204},
  number    = {10},
  pages     = {1413--1452},
  year      = {2006},
  url       = {https://doi.org/10.1016/j.ic.2005.05.009},
  doi       = {10.1016/j.ic.2005.05.009},
  timestamp = {Fri, 30 Nov 2018 00:00:00 +0100},
  biburl    = {https://dblp.org/rec/bib/journals/iandc/BaaderGT06},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/ijait/BaumgartnerFT06,
  author    = {Peter Baumgartner and
               Alexander Fuchs and
               Cesare Tinelli},
  title     = {Implementing the Model Evolution Calculus},
  journal   = {International Journal on Artificial Intelligence Tools},
  volume    = {15},
  number    = {1},
  pages     = {21--52},
  year      = {2006},
  url       = {https://doi.org/10.1142/S0218213006002552},
  doi       = {10.1142/S0218213006002552},
  timestamp = {Sun, 12 Nov 2017 00:00:00 +0100},
  biburl    = {https://dblp.org/rec/bib/journals/ijait/BaumgartnerFT06},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/jacm/NieuwenhuisOT06,
  author    = {Robert Nieuwenhuis and
               Albert Oliveras and
               Cesare Tinelli},
  title     = {Solving {SAT} and {SAT} Modulo Theories: From an abstract Davis--Putnam--Logemann--Loveland
               procedure to DPLL(\emph{T})},
  journal   = {J. {ACM}},
  volume    = {53},
  number    = {6},
  pages     = {937--977},
  year      = {2006},
  url       = {https://doi.org/10.1145/1217856.1217859},
  doi       = {10.1145/1217856.1217859},
  timestamp = {Tue, 06 Nov 2018 00:00:00 +0100},
  biburl    = {https://dblp.org/rec/bib/journals/jacm/NieuwenhuisOT06},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/lpar/BarrettNOT06,
  author    = {Clark Barrett and
               Robert Nieuwenhuis and
               Albert Oliveras and
               Cesare Tinelli},
  title     = {Splitting on Demand in {SAT} Modulo Theories},
  booktitle = {Logic for Programming, Artificial Intelligence, and Reasoning, 13th
               International Conference, {LPAR} 2006, Phnom Penh, Cambodia, November
               13-17, 2006, Proceedings},
  pages     = {512--526},
  year      = {2006},
  crossref  = {DBLP:conf/lpar/2006},
  url       = {https://doi.org/10.1007/11916277\_35},
  doi       = {10.1007/11916277\_35},
  timestamp = {Thu, 15 Jun 2017 01:00:00 +0200},
  biburl    = {https://dblp.org/rec/bib/conf/lpar/BarrettNOT06},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/lpar/BaumgartnerFT06,
  author    = {Peter Baumgartner and
               Alexander Fuchs and
               Cesare Tinelli},
  title     = {Lemma Learning in the Model Evolution Calculus},
  booktitle = {Logic for Programming, Artificial Intelligence, and Reasoning, 13th
               International Conference, {LPAR} 2006, Phnom Penh, Cambodia, November
               13-17, 2006, Proceedings},
  pages     = {572--586},
  year      = {2006},
  crossref  = {DBLP:conf/lpar/2006},
  url       = {https://doi.org/10.1007/11916277\_39},
  doi       = {10.1007/11916277\_39},
  timestamp = {Sun, 12 Nov 2017 00:00:00 +0100},
  biburl    = {https://dblp.org/rec/bib/conf/lpar/BaumgartnerFT06},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/entcs/AhrendtBNRT05,
  author    = {Wolfgang Ahrendt and
               Peter Baumgartner and
               Hans de Nivelle and
               Silvio Ranise and
               Cesare Tinelli},
  title     = {Preface},
  journal   = {Electr. Notes Theor. Comput. Sci.},
  volume    = {125},
  number    = {3},
  pages     = {1--2},
  year      = {2005},
  url       = {https://doi.org/10.1016/j.entcs.2005.02.025},
  doi       = {10.1016/j.entcs.2005.02.025},
  timestamp = {Sun, 12 Nov 2017 00:00:00 +0100},
  biburl    = {https://dblp.org/rec/bib/journals/entcs/AhrendtBNRT05},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/jar/TinelliZ05,
  author    = {Cesare Tinelli and
               Calogero G. Zarba},
  title     = {Combining Nonstably Infinite Theories},
  journal   = {J. Autom. Reasoning},
  volume    = {34},
  number    = {3},
  pages     = {209--238},
  year      = {2005},
  url       = {https://doi.org/10.1007/s10817-005-5204-9},
  doi       = {10.1007/s10817-005-5204-9},
  timestamp = {Thu, 15 Jun 2017 01:00:00 +0200},
  biburl    = {https://dblp.org/rec/bib/journals/jar/TinelliZ05},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cade/BaumgartnerT05,
  author    = {Peter Baumgartner and
               Cesare Tinelli},
  title     = {The Model Evolution Calculus with Equality},
  booktitle = {Automated Deduction - CADE-20, 20th International Conference on Automated
               Deduction, Tallinn, Estonia, July 22-27, 2005, Proceedings},
  pages     = {392--408},
  year      = {2005},
  crossref  = {DBLP:conf/cade/2005},
  url       = {https://doi.org/10.1007/11532231\_29},
  doi       = {10.1007/11532231\_29},
  timestamp = {Sun, 12 Nov 2017 00:00:00 +0100},
  biburl    = {https://dblp.org/rec/bib/conf/cade/BaumgartnerT05},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cade/BaaderGT04,
  author    = {Franz Baader and
               Silvio Ghilardi and
               Cesare Tinelli},
  title     = {A New Combination Procedure for the Word Problem That Generalizes
               Fusion Decidability Results in Modal Logics},
  booktitle = {Automated Reasoning - Second International Joint Conference, {IJCAR}
               2004, Cork, Ireland, July 4-8, 2004, Proceedings},
  pages     = {183--197},
  year      = {2004},
  crossref  = {DBLP:conf/cade/2004},
  url       = {https://doi.org/10.1007/978-3-540-25984-8\_11},
  doi       = {10.1007/978-3-540-25984-8\_11},
  timestamp = {Thu, 15 Jun 2017 01:00:00 +0200},
  biburl    = {https://dblp.org/rec/bib/conf/cade/BaaderGT04},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cav/GanzingerHNOT04,
  author    = {Harald Ganzinger and
               George Hagen and
               Robert Nieuwenhuis and
               Albert Oliveras and
               Cesare Tinelli},
  title     = {{DPLL(} {T):} Fast Decision Procedures},
  booktitle = {Computer Aided Verification, 16th International Conference, {CAV}
               2004, Boston, MA, USA, July 13-17, 2004, Proceedings},
  pages     = {175--188},
  year      = {2004},
  crossref  = {DBLP:conf/cav/2004},
  url       = {https://doi.org/10.1007/978-3-540-27813-9\_14},
  doi       = {10.1007/978-3-540-27813-9\_14},
  timestamp = {Thu, 15 Jun 2017 01:00:00 +0200},
  biburl    = {https://dblp.org/rec/bib/conf/cav/GanzingerHNOT04},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/jelia/TinelliZ04,
  author    = {Cesare Tinelli and
               Calogero G. Zarba},
  title     = {Combining Decision Procedures for Sorted Theories},
  booktitle = {Logics in Artificial Intelligence, 9th European Conference, {JELIA}
               2004, Lisbon, Portugal, September 27-30, 2004, Proceedings},
  pages     = {641--653},
  year      = {2004},
  crossref  = {DBLP:conf/jelia/2004},
  url       = {https://doi.org/10.1007/978-3-540-30227-8\_53},
  doi       = {10.1007/978-3-540-30227-8\_53},
  timestamp = {Thu, 15 Jun 2017 01:00:00 +0200},
  biburl    = {https://dblp.org/rec/bib/conf/jelia/TinelliZ04},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/lpar/NieuwenhuisOT04,
  author    = {Robert Nieuwenhuis and
               Albert Oliveras and
               Cesare Tinelli},
  title     = {Abstract {DPLL} and Abstract {DPLL} Modulo Theories},
  booktitle = {Logic for Programming, Artificial Intelligence, and Reasoning, 11th
               International Conference, {LPAR} 2004, Montevideo, Uruguay, March
               14-18, 2005, Proceedings},
  pages     = {36--50},
  year      = {2004},
  crossref  = {DBLP:conf/lpar/2004},
  url       = {https://doi.org/10.1007/978-3-540-32275-7\_3},
  doi       = {10.1007/978-3-540-32275-7\_3},
  timestamp = {Thu, 15 Jun 2017 01:00:00 +0200},
  biburl    = {https://dblp.org/rec/bib/conf/lpar/NieuwenhuisOT04},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/entcs/TinelliZ03,
  author    = {Cesare Tinelli and
               Calogero G. Zarba},
  title     = {Combining Non-Stably Infinite Theories},
  journal   = {Electr. Notes Theor. Comput. Sci.},
  volume    = {86},
  number    = {1},
  pages     = {35--48},
  year      = {2003},
  url       = {https://doi.org/10.1016/S1571-0661(04)80651-0},
  doi       = {10.1016/S1571-0661(04)80651-0},
  timestamp = {Wed, 14 Jun 2017 01:00:00 +0200},
  biburl    = {https://dblp.org/rec/bib/journals/entcs/TinelliZ03},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/jar/Tinelli03,
  author    = {Cesare Tinelli},
  title     = {Cooperation of Background Reasoners in Theory Reasoning by Residue
               Sharing},
  journal   = {J. Autom. Reasoning},
  volume    = {30},
  number    = {1},
  pages     = {1--31},
  year      = {2003},
  url       = {https://doi.org/10.1023/A:1022587501759},
  doi       = {10.1023/A:1022587501759},
  timestamp = {Sat, 20 May 2017 01:00:00 +0200},
  biburl    = {https://dblp.org/rec/bib/journals/jar/Tinelli03},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/tcs/TinelliR03,
  author    = {Cesare Tinelli and
               Christophe Ringeissen},
  title     = {Unions of non-disjoint theories and combinations of satisfiability
               procedures},
  journal   = {Theor. Comput. Sci.},
  volume    = {290},
  number    = {1},
  pages     = {291--353},
  year      = {2003},
  url       = {https://doi.org/10.1016/S0304-3975(01)00332-2},
  doi       = {10.1016/S0304-3975(01)00332-2},
  timestamp = {Wed, 14 Jun 2017 01:00:00 +0200},
  biburl    = {https://dblp.org/rec/bib/journals/tcs/TinelliR03},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/tcs/TinelliR03a,
  author    = {Cesare Tinelli and
               Teodor Rus},
  title     = {Preface},
  journal   = {Theor. Comput. Sci.},
  volume    = {291},
  number    = {3},
  pages     = {219--221},
  year      = {2003},
  url       = {https://doi.org/10.1016/S0304-3975(02)00363-8},
  doi       = {10.1016/S0304-3975(02)00363-8},
  timestamp = {Wed, 14 Jun 2017 01:00:00 +0200},
  biburl    = {https://dblp.org/rec/bib/journals/tcs/TinelliR03a},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cade/BaumgartnerT03,
  author    = {Peter Baumgartner and
               Cesare Tinelli},
  title     = {The Model Evolution Calculus},
  booktitle = {Automated Deduction - CADE-19, 19th International Conference on Automated
               Deduction Miami Beach, FL, USA, July 28 - August 2, 2003, Proceedings},
  pages     = {350--364},
  year      = {2003},
  crossref  = {DBLP:conf/cade/2003},
  url       = {https://doi.org/10.1007/978-3-540-45085-6\_32},
  doi       = {10.1007/978-3-540-45085-6\_32},
  timestamp = {Sun, 12 Nov 2017 00:00:00 +0100},
  biburl    = {https://dblp.org/rec/bib/conf/cade/BaumgartnerT03},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/iandc/BaaderT02,
  author    = {Franz Baader and
               Cesare Tinelli},
  title     = {Deciding the Word Problem in the Union of Equational Theories},
  journal   = {Inf. Comput.},
  volume    = {178},
  number    = {2},
  pages     = {346--390},
  year      = {2002},
  url       = {https://doi.org/10.1006/inco.2001.3118},
  doi       = {10.1006/inco.2001.3118},
  timestamp = {Wed, 14 Nov 2018 00:00:00 +0100},
  biburl    = {https://dblp.org/rec/bib/journals/iandc/BaaderT02},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/jelia/Tinelli02,
  author    = {Cesare Tinelli},
  title     = {A DPLL-Based Calculus for Ground Satisfiability Modulo Theories},
  booktitle = {Logics in Artificial Intelligence, European Conference, {JELIA} 2002,
               Cosenza, Italy, September, 23-26, Proceedings},
  pages     = {308--319},
  year      = {2002},
  crossref  = {DBLP:conf/jelia/2002},
  url       = {https://doi.org/10.1007/3-540-45757-7\_26},
  doi       = {10.1007/3-540-45757-7\_26},
  timestamp = {Thu, 15 Jun 2017 21:42:21 +0200},
  biburl    = {https://dblp.org/rec/bib/conf/jelia/Tinelli02},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/rta/BaaderT02,
  author    = {Franz Baader and
               Cesare Tinelli},
  title     = {Combining Decision Procedures for Positive Theories Sharing Constructors},
  booktitle = {Rewriting Techniques and Applications, 13th International Conference,
               {RTA} 2002, Copenhagen, Denmark, July 22-24, 2002, Proceedings},
  pages     = {352--366},
  year      = {2002},
  crossref  = {DBLP:conf/rta/2002},
  url       = {https://doi.org/10.1007/3-540-45610-4\_25},
  doi       = {10.1007/3-540-45610-4\_25},
  timestamp = {Thu, 15 Jun 2017 21:39:22 +0200},
  biburl    = {https://dblp.org/rec/bib/conf/rta/BaaderT02},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/frocos/BaaderT00,
  author    = {Franz Baader and
               Cesare Tinelli},
  title     = {Combining Equational Theories Sharing Non-Collapse-Free Constructors},
  booktitle = {Frontiers of Combining Systems, Third International Workshop, FroCoS
               2000, Nancy, France, March 22-24, 2000, Proceedings},
  pages     = {260--274},
  year      = {2000},
  crossref  = {DBLP:conf/frocos/2000},
  url       = {https://doi.org/10.1007/10720084\_17},
  doi       = {10.1007/10720084\_17},
  timestamp = {Thu, 15 Jun 2017 01:00:00 +0200},
  biburl    = {https://dblp.org/rec/bib/conf/frocos/BaaderT00},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/rta/BaaderT99,
  author    = {Franz Baader and
               Cesare Tinelli},
  title     = {Deciding the Word Problem in the Union of Equational Theories Sharing
               Constructors},
  booktitle = {Rewriting Techniques and Applications, 10th International Conference,
               RTA-99, Trento, Italy, July 2-4, 1999, Proceedings},
  pages     = {175--189},
  year      = {1999},
  crossref  = {DBLP:conf/rta/1999},
  url       = {https://doi.org/10.1007/3-540-48685-2\_14},
  doi       = {10.1007/3-540-48685-2\_14},
  timestamp = {Thu, 15 Jun 2017 01:00:00 +0200},
  biburl    = {https://dblp.org/rec/bib/conf/rta/BaaderT99},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/jflp/TinelliH98,
  author    = {Cesare Tinelli and
               Mehdi T. Harandi},
  title     = {Constraint Logic Programming over Unions of Constraint Theories},
  journal   = {Journal of Functional and Logic Programming},
  volume    = {1998},
  number    = {6},
  year      = {1998},
  url       = {http://danae.uni-muenster.de/lehre/kuchen/JFLP/articles/1998/A98-06/A98-06.html},
  timestamp = {Fri, 21 Dec 2012 00:00:00 +0100},
  biburl    = {https://dblp.org/rec/bib/journals/jflp/TinelliH98},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cade/BaaderT97,
  author    = {Franz Baader and
               Cesare Tinelli},
  title     = {A New Approach for Combining Decision Procedure for the Word Problem,
               and Its Connection to the Nelson-Oppen Combination Method},
  booktitle = {Automated Deduction - CADE-14, 14th International Conference on Automated
               Deduction, Townsville, North Queensland, Australia, July 13-17, 1997,
               Proceedings},
  pages     = {19--33},
  year      = {1997},
  crossref  = {DBLP:conf/cade/1997},
  url       = {https://doi.org/10.1007/3-540-63104-6\_3},
  doi       = {10.1007/3-540-63104-6\_3},
  timestamp = {Thu, 15 Jun 2017 01:00:00 +0200},
  biburl    = {https://dblp.org/rec/bib/conf/cade/BaaderT97},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cp/TinelliH96,
  author    = {Cesare Tinelli and
               Mehdi T. Harandi},
  title     = {Constraint Logic Programming over Unions of Constraint Theories},
  booktitle = {Proceedings of the Second International Conference on Principles and
               Practice of Constraint Programming, Cambridge, Massachusetts, USA,
               August 19-22, 1996},
  pages     = {436--450},
  year      = {1996},
  crossref  = {DBLP:conf/cp/1996},
  url       = {https://doi.org/10.1007/3-540-61551-2\_92},
  doi       = {10.1007/3-540-61551-2\_92},
  timestamp = {Thu, 15 Jun 2017 01:00:00 +0200},
  biburl    = {https://dblp.org/rec/bib/conf/cp/TinelliH96},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/frocos/TinelliH96,
  author    = {Cesare Tinelli and
               Mehdi T. Harandi},
  title     = {A New Correctness Proof of the \{Nelson-Oppen\} Combination Procedure},
  booktitle = {Frontiers of Combining Systems, First International Workshop FroCoS
               1996, Munich, Germany, March 26-29, 1996, Proceedings},
  pages     = {103--119},
  year      = {1996},
  crossref  = {DBLP:conf/frocos/1996},
  timestamp = {Mon, 20 Mar 2017 13:54:49 +0100},
  biburl    = {https://dblp.org/rec/bib/conf/frocos/TinelliH96},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@proceedings{DBLP:conf/cade/2018,
  editor    = {Didier Galmiche and
               Stephan Schulz and
               Roberto Sebastiani},
  title     = {Automated Reasoning - 9th International Joint Conference, {IJCAR}
               2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford,
               UK, July 14-17, 2018, Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {10900},
  publisher = {Springer},
  year      = {2018},
  url       = {https://doi.org/10.1007/978-3-319-94205-6},
  doi       = {10.1007/978-3-319-94205-6},
  isbn      = {978-3-319-94204-9},
  timestamp = {Mon, 09 Jul 2018 12:59:13 +0200},
  biburl    = {https://dblp.org/rec/bib/conf/cade/2018},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@proceedings{DBLP:conf/cav/2018-2,
  editor    = {Hana Chockler and
               Georg Weissenbacher},
  title     = {Computer Aided Verification - 30th International Conference, {CAV}
               2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford,
               UK, July 14-17, 2018, Proceedings, Part {II}},
  series    = {Lecture Notes in Computer Science},
  volume    = {10982},
  publisher = {Springer},
  year      = {2018},
  url       = {https://doi.org/10.1007/978-3-319-96142-2},
  doi       = {10.1007/978-3-319-96142-2},
  isbn      = {978-3-319-96141-5},
  timestamp = {Mon, 23 Jul 2018 17:21:41 +0200},
  biburl    = {https://dblp.org/rec/bib/conf/cav/2018-2},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@book{DBLP:reference/mc/2018,
  editor    = {Edmund M. Clarke and
               Thomas A. Henzinger and
               Helmut Veith and
               Roderick Bloem},
  title     = {Handbook of Model Checking},
  publisher = {Springer},
  year      = {2018},
  url       = {https://doi.org/10.1007/978-3-319-10575-8},
  doi       = {10.1007/978-3-319-10575-8},
  isbn      = {978-3-319-10574-1},
  timestamp = {Tue, 29 May 2018 12:30:27 +0200},
  biburl    = {https://dblp.org/rec/bib/reference/mc/2018},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@proceedings{DBLP:conf/cade/2017,
  editor    = {Leonardo de Moura},
  title     = {Automated Deduction - {CADE} 26 - 26th International Conference on
               Automated Deduction, Gothenburg, Sweden, August 6-11, 2017, Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {10395},
  publisher = {Springer},
  year      = {2017},
  url       = {https://doi.org/10.1007/978-3-319-63046-5},
  doi       = {10.1007/978-3-319-63046-5},
  isbn      = {978-3-319-63045-8},
  timestamp = {Wed, 12 Jul 2017 10:06:41 +0200},
  biburl    = {https://dblp.org/rec/bib/conf/cade/2017},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@proceedings{DBLP:conf/cav/2017-2,
  editor    = {Rupak Majumdar and
               Viktor Kuncak},
  title     = {Computer Aided Verification - 29th International Conference, {CAV}
               2017, Heidelberg, Germany, July 24-28, 2017, Proceedings, Part {II}},
  series    = {Lecture Notes in Computer Science},
  volume    = {10427},
  publisher = {Springer},
  year      = {2017},
  url       = {https://doi.org/10.1007/978-3-319-63390-9},
  doi       = {10.1007/978-3-319-63390-9},
  isbn      = {978-3-319-63389-3},
  timestamp = {Fri, 14 Jul 2017 13:04:29 +0200},
  biburl    = {https://dblp.org/rec/bib/conf/cav/2017-2},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@proceedings{DBLP:conf/frocos/2017,
  editor    = {Clare Dixon and
               Marcelo Finger},
  title     = {Frontiers of Combining Systems - 11th International Symposium, FroCoS
               2017, Bras{\'{\i}}lia, Brazil, September 27-29, 2017, Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {10483},
  publisher = {Springer},
  year      = {2017},
  url       = {https://doi.org/10.1007/978-3-319-66167-4},
  doi       = {10.1007/978-3-319-66167-4},
  isbn      = {978-3-319-66166-7},
  timestamp = {Tue, 05 Sep 2017 14:29:33 +0200},
  biburl    = {https://dblp.org/rec/bib/conf/frocos/2017},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@proceedings{DBLP:conf/nfm/2017,
  editor    = {Clark Barrett and
               Misty Davies and
               Temesghen Kahsai},
  title     = {{NASA} Formal Methods - 9th International Symposium, {NFM} 2017, Moffett
               Field, CA, USA, May 16-18, 2017, Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {10227},
  year      = {2017},
  url       = {https://doi.org/10.1007/978-3-319-57288-8},
  doi       = {10.1007/978-3-319-57288-8},
  isbn      = {978-3-319-57287-1},
  timestamp = {Thu, 25 May 2017 00:40:09 +0200},
  biburl    = {https://dblp.org/rec/bib/conf/nfm/2017},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@proceedings{DBLP:journals/corr/abs-1711-10224,
  editor    = {Dana Fisman and
               Swen Jacobs},
  title     = {Proceedings Sixth Workshop on Synthesis, SYNT@CAV 2017, Heidelberg,
               Germany, 22nd July 2017},
  series    = {{EPTCS}},
  volume    = {260},
  year      = {2017},
  url       = {http://arxiv.org/abs/1711.10224},
  timestamp = {Mon, 13 Aug 2018 16:48:22 +0200},
  biburl    = {https://dblp.org/rec/bib/journals/corr/abs-1711-10224},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@proceedings{DBLP:conf/cade/2016,
  editor    = {Nicola Olivetti and
               Ashish Tiwari},
  title     = {Automated Reasoning - 8th International Joint Conference, {IJCAR}
               2016, Coimbra, Portugal, June 27 - July 2, 2016, Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {9706},
  publisher = {Springer},
  year      = {2016},
  url       = {https://doi.org/10.1007/978-3-319-40229-1},
  doi       = {10.1007/978-3-319-40229-1},
  isbn      = {978-3-319-40228-4},
  timestamp = {Sun, 21 May 2017 00:17:18 +0200},
  biburl    = {https://dblp.org/rec/bib/conf/cade/2016},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@proceedings{DBLP:conf/cav/2016-2,
  editor    = {Swarat Chaudhuri and
               Azadeh Farzan},
  title     = {Computer Aided Verification - 28th International Conference, {CAV}
               2016, Toronto, ON, Canada, July 17-23, 2016, Proceedings, Part {II}},
  series    = {Lecture Notes in Computer Science},
  volume    = {9780},
  publisher = {Springer},
  year      = {2016},
  url       = {https://doi.org/10.1007/978-3-319-41540-6},
  doi       = {10.1007/978-3-319-41540-6},
  isbn      = {978-3-319-41539-0},
  timestamp = {Thu, 25 May 2017 00:39:07 +0200},
  biburl    = {https://dblp.org/rec/bib/conf/cav/2016-2},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@proceedings{DBLP:conf/fmcad/2016,
  editor    = {Ruzica Piskac and
               Muralidhar Talupur},
  title     = {2016 Formal Methods in Computer-Aided Design, {FMCAD} 2016, Mountain
               View, CA, USA, October 3-6, 2016},
  publisher = {{IEEE}},
  year      = {2016},
  url       = {http://ieeexplore.ieee.org/xpl/mostRecentIssue.jsp?punumber=7879555},
  isbn      = {978-0-9835678-6-8},
  timestamp = {Fri, 31 Mar 2017 11:38:24 +0200},
  biburl    = {https://dblp.org/rec/bib/conf/fmcad/2016},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@proceedings{DBLP:conf/hotsos/2016,
  editor    = {William L. Scherlis and
               David Brumley},
  title     = {Proceedings of the Symposium and Bootcamp on the Science of Security,
               Pittsburgh, PA, USA, April 19-21, 2016},
  publisher = {{ACM}},
  year      = {2016},
  url       = {http://dl.acm.org/citation.cfm?id=2898375},
  isbn      = {978-1-4503-4277-3},
  timestamp = {Fri, 22 Apr 2016 13:50:41 +0200},
  biburl    = {https://dblp.org/rec/bib/conf/hotsos/2016},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@proceedings{DBLP:conf/sefm/2016,
  editor    = {Rocco {De Nicola} and
               eva K{\"{u}}hn},
  title     = {Software Engineering and Formal Methods - 14th International Conference,
               {SEFM} 2016, Held as Part of {STAF} 2016, Vienna, Austria, July 4-8,
               2016, Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {9763},
  publisher = {Springer},
  year      = {2016},
  url       = {https://doi.org/10.1007/978-3-319-41591-8},
  doi       = {10.1007/978-3-319-41591-8},
  isbn      = {978-3-319-41590-1},
  timestamp = {Sun, 21 May 2017 00:18:56 +0200},
  biburl    = {https://dblp.org/rec/bib/conf/sefm/2016},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@proceedings{DBLP:journals/corr/BlanchetteK16,
  editor    = {Jasmin Christian Blanchette and
               Cezary Kaliszyk},
  title     = {Proceedings First International Workshop on Hammers for Type Theories,
               HaTT@IJCAR 2016, Coimbra, Portugal, July 1, 2016},
  series    = {{EPTCS}},
  volume    = {210},
  year      = {2016},
  url       = {https://doi.org/10.4204/EPTCS.210},
  doi       = {10.4204/EPTCS.210},
  timestamp = {Wed, 12 Sep 2018 01:05:14 +0200},
  biburl    = {https://dblp.org/rec/bib/journals/corr/BlanchetteK16},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@proceedings{DBLP:conf/arith/2015,
  title     = {22nd {IEEE} Symposium on Computer Arithmetic, {ARITH} 2015, Lyon,
               France, June 22-24, 2015},
  publisher = {{IEEE}},
  year      = {2015},
  url       = {http://ieeexplore.ieee.org/xpl/mostRecentIssue.jsp?punumber=7193754},
  isbn      = {978-1-4799-8664-4},
  timestamp = {Thu, 27 Aug 2015 17:03:25 +0200},
  biburl    = {https://dblp.org/rec/bib/conf/arith/2015},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@proceedings{DBLP:conf/cav/2015,
  editor    = {Daniel Kroening and
               Corina S. Pasareanu},
  title     = {Computer Aided Verification - 27th International Conference, {CAV}
               2015, San Francisco, CA, USA, July 18-24, 2015, Proceedings, Part
               {II}},
  series    = {Lecture Notes in Computer Science},
  volume    = {9207},
  publisher = {Springer},
  year      = {2015},
  url       = {https://doi.org/10.1007/978-3-319-21668-3},
  doi       = {10.1007/978-3-319-21668-3},
  isbn      = {978-3-319-21667-6},
  timestamp = {Thu, 25 May 2017 00:39:07 +0200},
  biburl    = {https://dblp.org/rec/bib/conf/cav/2015},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@proceedings{DBLP:conf/frocos/2015,
  editor    = {Carsten Lutz and
               Silvio Ranise},
  title     = {Frontiers of Combining Systems - 10th International Symposium, FroCoS
               2015, Wroclaw, Poland, September 21-24, 2015. Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {9322},
  publisher = {Springer},
  year      = {2015},
  url       = {https://doi.org/10.1007/978-3-319-24246-0},
  doi       = {10.1007/978-3-319-24246-0},
  isbn      = {978-3-319-24245-3},
  timestamp = {Thu, 15 Jun 2017 21:43:48 +0200},
  biburl    = {https://dblp.org/rec/bib/conf/frocos/2015},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@proceedings{DBLP:conf/lpar/2015,
  editor    = {Martin Davis and
               Ansgar Fehnker and
               Annabelle McIver and
               Andrei Voronkov},
  title     = {Logic for Programming, Artificial Intelligence, and Reasoning - 20th
               International Conference, {LPAR-20} 2015, Suva, Fiji, November 24-28,
               2015, Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {9450},
  publisher = {Springer},
  year      = {2015},
  url       = {https://doi.org/10.1007/978-3-662-48899-7},
  doi       = {10.1007/978-3-662-48899-7},
  isbn      = {978-3-662-48898-0},
  timestamp = {Fri, 02 Nov 2018 09:44:58 +0100},
  biburl    = {https://dblp.org/rec/bib/conf/lpar/2015},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@proceedings{DBLP:conf/cade/2014,
  editor    = {St{\'{e}}phane Demri and
               Deepak Kapur and
               Christoph Weidenbach},
  title     = {Automated Reasoning - 7th International Joint Conference, {IJCAR}
               2014, Held as Part of the Vienna Summer of Logic, {VSL} 2014, Vienna,
               Austria, July 19-22, 2014. Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {8562},
  publisher = {Springer},
  year      = {2014},
  url       = {https://doi.org/10.1007/978-3-319-08587-6},
  doi       = {10.1007/978-3-319-08587-6},
  isbn      = {978-3-319-08586-9},
  timestamp = {Sun, 21 May 2017 00:17:17 +0200},
  biburl    = {https://dblp.org/rec/bib/conf/cade/2014},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@proceedings{DBLP:conf/cav/2014,
  editor    = {Armin Biere and
               Roderick Bloem},
  title     = {Computer Aided Verification - 26th International Conference, {CAV}
               2014, Held as Part of the Vienna Summer of Logic, {VSL} 2014, Vienna,
               Austria, July 18-22, 2014. Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {8559},
  publisher = {Springer},
  year      = {2014},
  url       = {https://doi.org/10.1007/978-3-319-08867-9},
  doi       = {10.1007/978-3-319-08867-9},
  isbn      = {978-3-319-08866-2},
  timestamp = {Thu, 25 May 2017 00:39:07 +0200},
  biburl    = {https://dblp.org/rec/bib/conf/cav/2014},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@proceedings{DBLP:conf/fmcad/2014,
  title     = {Formal Methods in Computer-Aided Design, {FMCAD} 2014, Lausanne, Switzerland,
               October 21-24, 2014},
  publisher = {{IEEE}},
  year      = {2014},
  url       = {http://ieeexplore.ieee.org/xpl/mostRecentIssue.jsp?punumber=6975680},
  isbn      = {978-0-9835678-4-4},
  timestamp = {Thu, 08 Jan 2015 11:21:45 +0100},
  biburl    = {https://dblp.org/rec/bib/conf/fmcad/2014},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@proceedings{DBLP:conf/smt/2014,
  editor    = {Philipp R{\"{u}}mmer and
               Christoph M. Wintersteiger},
  title     = {Proceedings of the 12th International Workshop on Satisfiability Modulo
               Theories, {SMT} 2014, affiliated with the 26th International Conference
               on Computer Aided Verification {(CAV} 2014), the 7th International
               Joint Conference on Automated Reasoning {(IJCAR} 2014), and the 17th
               International Conference on Theory and Applications of Satisfiability
               Testing {(SAT} 2014), Vienna, Austria, July 17-18, 2014},
  series    = {{CEUR} Workshop Proceedings},
  volume    = {1163},
  publisher = {CEUR-WS.org},
  year      = {2014},
  url       = {http://ceur-ws.org/Vol-1163},
  urn       = {urn:nbn:de:0074-1163-4},
  timestamp = {Mon, 30 May 2016 16:28:37 +0200},
  biburl    = {https://dblp.org/rec/bib/conf/smt/2014},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@proceedings{DBLP:conf/cade/2013,
  editor    = {Maria Paola Bonacina},
  title     = {Automated Deduction - {CADE-24} - 24th International Conference on
               Automated Deduction, Lake Placid, NY, USA, June 9-14, 2013. Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {7898},
  publisher = {Springer},
  year      = {2013},
  url       = {https://doi.org/10.1007/978-3-642-38574-2},
  doi       = {10.1007/978-3-642-38574-2},
  isbn      = {978-3-642-38573-5},
  timestamp = {Sun, 21 May 2017 00:17:17 +0200},
  biburl    = {https://dblp.org/rec/bib/conf/cade/2013},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@proceedings{DBLP:conf/cav/2013,
  editor    = {Natasha Sharygina and
               Helmut Veith},
  title     = {Computer Aided Verification - 25th International Conference, {CAV}
               2013, Saint Petersburg, Russia, July 13-19, 2013. Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {8044},
  publisher = {Springer},
  year      = {2013},
  url       = {https://doi.org/10.1007/978-3-642-39799-8},
  doi       = {10.1007/978-3-642-39799-8},
  isbn      = {978-3-642-39798-1},
  timestamp = {Thu, 25 May 2017 00:39:06 +0200},
  biburl    = {https://dblp.org/rec/bib/conf/cav/2013},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@proceedings{DBLP:conf/nfm/2013,
  editor    = {Guillaume Brat and
               Neha Rungta and
               Arnaud Venet},
  title     = {{NASA} Formal Methods, 5th International Symposium, {NFM} 2013, Moffett
               Field, CA, USA, May 14-16, 2013. Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {7871},
  publisher = {Springer},
  year      = {2013},
  url       = {https://doi.org/10.1007/978-3-642-38088-4},
  doi       = {10.1007/978-3-642-38088-4},
  isbn      = {978-3-642-38087-7},
  timestamp = {Thu, 25 May 2017 00:40:09 +0200},
  biburl    = {https://dblp.org/rec/bib/conf/nfm/2013},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@proceedings{DBLP:conf/cade/2012compare,
  editor    = {Vladimir Klebanov and
               Bernhard Beckert and
               Armin Biere and
               Geoff Sutcliffe},
  title     = {Proceedings of the 1st International Workshop on Comparative Empirical
               Evaluation of Reasoning Systems, Manchester, United Kingdom, June
               30, 2012},
  series    = {{CEUR} Workshop Proceedings},
  volume    = {873},
  publisher = {CEUR-WS.org},
  year      = {2012},
  url       = {http://ceur-ws.org/Vol-873},
  urn       = {urn:nbn:de:0074-873-1},
  timestamp = {Mon, 30 May 2016 16:43:12 +0200},
  biburl    = {https://dblp.org/rec/bib/conf/cade/2012compare},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@proceedings{DBLP:conf/cade/2012paar,
  editor    = {Pascal Fontaine and
               Renate A. Schmidt and
               Stephan Schulz},
  title     = {Third Workshop on Practical Aspects of Automated Reasoning, PAAR-2012,
               Manchester, UK, June 30 - July 1, 2012},
  series    = {EPiC Series in Computing},
  volume    = {21},
  publisher = {EasyChair},
  year      = {2013},
  url       = {http://www.easychair.org/publications/?page=1924317986},
  timestamp = {Wed, 29 Mar 2017 16:45:22 +0200},
  biburl    = {https://dblp.org/rec/bib/conf/cade/2012paar},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@proceedings{DBLP:conf/nfm/2012,
  editor    = {Alwyn Goodloe and
               Suzette Person},
  title     = {{NASA} Formal Methods - 4th International Symposium, {NFM} 2012, Norfolk,
               VA, USA, April 3-5, 2012. Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {7226},
  publisher = {Springer},
  year      = {2012},
  url       = {https://doi.org/10.1007/978-3-642-28891-3},
  doi       = {10.1007/978-3-642-28891-3},
  isbn      = {978-3-642-28890-6},
  timestamp = {Thu, 25 May 2017 00:40:09 +0200},
  biburl    = {https://dblp.org/rec/bib/conf/nfm/2012},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@proceedings{DBLP:conf/cade/2011,
  editor    = {Nikolaj Bj{\o}rner and
               Viorica Sofronie{-}Stokkermans},
  title     = {Automated Deduction - {CADE-23} - 23rd International Conference on
               Automated Deduction, Wroclaw, Poland, July 31 - August 5, 2011. Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {6803},
  publisher = {Springer},
  year      = {2011},
  url       = {https://doi.org/10.1007/978-3-642-22438-6},
  doi       = {10.1007/978-3-642-22438-6},
  isbn      = {978-3-642-22437-9},
  timestamp = {Sun, 21 May 2017 00:17:18 +0200},
  biburl    = {https://dblp.org/rec/bib/conf/cade/2011},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@proceedings{DBLP:conf/cav/2011,
  editor    = {Ganesh Gopalakrishnan and
               Shaz Qadeer},
  title     = {Computer Aided Verification - 23rd International Conference, {CAV}
               2011, Snowbird, UT, USA, July 14-20, 2011. Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {6806},
  publisher = {Springer},
  year      = {2011},
  url       = {https://doi.org/10.1007/978-3-642-22110-1},
  doi       = {10.1007/978-3-642-22110-1},
  isbn      = {978-3-642-22109-5},
  timestamp = {Thu, 25 May 2017 00:39:08 +0200},
  biburl    = {https://dblp.org/rec/bib/conf/cav/2011},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@proceedings{DBLP:conf/nfm/2011,
  editor    = {Mihaela Gheorghiu Bobaru and
               Klaus Havelund and
               Gerard J. Holzmann and
               Rajeev Joshi},
  title     = {{NASA} Formal Methods - Third International Symposium, {NFM} 2011,
               Pasadena, CA, USA, April 18-20, 2011. Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {6617},
  publisher = {Springer},
  year      = {2011},
  url       = {https://doi.org/10.1007/978-3-642-20398-5},
  doi       = {10.1007/978-3-642-20398-5},
  isbn      = {978-3-642-20397-8},
  timestamp = {Thu, 25 May 2017 00:40:10 +0200},
  biburl    = {https://dblp.org/rec/bib/conf/nfm/2011},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@proceedings{DBLP:journals/corr/abs-1111-0064,
  editor    = {Jiri Barnat and
               Keijo Heljanko},
  title     = {Proceedings 10th International Workshop on Parallel and Distributed
               Methods in verifiCation, {PDMC} 2011, Snowbird, Utah, USA, July 14,
               2011},
  series    = {{EPTCS}},
  volume    = {72},
  year      = {2011},
  url       = {https://doi.org/10.4204/EPTCS.72},
  doi       = {10.4204/EPTCS.72},
  timestamp = {Wed, 12 Sep 2018 01:05:14 +0200},
  biburl    = {https://dblp.org/rec/bib/journals/corr/abs-1111-0064},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@proceedings{DBLP:conf/hvc/2010,
  editor    = {Sharon Barner and
               Ian G. Harris and
               Daniel Kroening and
               Orna Raz},
  title     = {Hardware and Software: Verification and Testing - 6th International
               Haifa Verification Conference, {HVC} 2010, Haifa, Israel, October
               4-7, 2010. Revised Selected Papers},
  series    = {Lecture Notes in Computer Science},
  volume    = {6504},
  publisher = {Springer},
  year      = {2011},
  url       = {https://doi.org/10.1007/978-3-642-19583-9},
  doi       = {10.1007/978-3-642-19583-9},
  isbn      = {978-3-642-19582-2},
  timestamp = {Fri, 19 May 2017 01:26:09 +0200},
  biburl    = {https://dblp.org/rec/bib/conf/hvc/2010},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@proceedings{DBLP:conf/wollic/2010,
  editor    = {Anuj Dawar and
               Ruy J. G. B. de Queiroz},
  title     = {Logic, Language, Information and Computation, 17th International Workshop,
               WoLLIC 2010, Brasilia, Brazil, July 6-9, 2010. Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {6188},
  publisher = {Springer},
  year      = {2010},
  url       = {https://doi.org/10.1007/978-3-642-13824-9},
  doi       = {10.1007/978-3-642-13824-9},
  isbn      = {978-3-642-13823-2},
  timestamp = {Wed, 14 Nov 2018 10:55:35 +0100},
  biburl    = {https://dblp.org/rec/bib/conf/wollic/2010},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@proceedings{DBLP:conf/cade/2009,
  editor    = {Renate A. Schmidt},
  title     = {Automated Deduction - CADE-22, 22nd International Conference on Automated
               Deduction, Montreal, Canada, August 2-7, 2009. Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {5663},
  publisher = {Springer},
  year      = {2009},
  url       = {https://doi.org/10.1007/978-3-642-02959-2},
  doi       = {10.1007/978-3-642-02959-2},
  isbn      = {978-3-642-02958-5},
  timestamp = {Sun, 21 May 2017 00:17:18 +0200},
  biburl    = {https://dblp.org/rec/bib/conf/cade/2009},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@proceedings{DBLP:conf/tacas/2009,
  editor    = {Stefan Kowalewski and
               Anna Philippou},
  title     = {Tools and Algorithms for the Construction and Analysis of Systems,
               15th International Conference, {TACAS} 2009, Held as Part of the Joint
               European Conferences on Theory and Practice of Software, {ETAPS} 2009,
               York, UK, March 22-29, 2009. Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {5505},
  publisher = {Springer},
  year      = {2009},
  url       = {https://doi.org/10.1007/978-3-642-00768-2},
  doi       = {10.1007/978-3-642-00768-2},
  isbn      = {978-3-642-00767-5},
  timestamp = {Wed, 24 May 2017 08:28:32 +0200},
  biburl    = {https://dblp.org/rec/bib/conf/tacas/2009},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@proceedings{DBLP:series/faia/2009-185,
  editor    = {Armin Biere and
               Marijn Heule and
               Hans van Maaren and
               Toby Walsh},
  title     = {Handbook of Satisfiability},
  series    = {Frontiers in Artificial Intelligence and Applications},
  volume    = {185},
  publisher = {{IOS} Press},
  year      = {2009},
  isbn      = {978-1-58603-929-5},
  timestamp = {Wed, 16 Sep 2009 11:21:15 +0200},
  biburl    = {https://dblp.org/rec/bib/series/faia/2009-185},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@proceedings{DBLP:conf/fmcad/2008,
  editor    = {Alessandro Cimatti and
               Robert B. Jones},
  title     = {Formal Methods in Computer-Aided Design, {FMCAD} 2008, Portland, Oregon,
               USA, 17-20 November 2008},
  publisher = {{IEEE}},
  year      = {2008},
  url       = {http://ieeexplore.ieee.org/xpl/mostRecentIssue.jsp?punumber=4689158},
  isbn      = {978-1-4244-2735-2},
  timestamp = {Wed, 17 Feb 2016 13:08:35 +0100},
  biburl    = {https://dblp.org/rec/bib/conf/fmcad/2008},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@proceedings{DBLP:conf/lpar/2008,
  editor    = {Iliano Cervesato and
               Helmut Veith and
               Andrei Voronkov},
  title     = {Logic for Programming, Artificial Intelligence, and Reasoning, 15th
               International Conference, {LPAR} 2008, Doha, Qatar, November 22-27,
               2008. Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {5330},
  publisher = {Springer},
  year      = {2008},
  url       = {https://doi.org/10.1007/978-3-540-89439-1},
  doi       = {10.1007/978-3-540-89439-1},
  isbn      = {978-3-540-89438-4},
  timestamp = {Tue, 13 Jun 2017 10:37:56 +0200},
  biburl    = {https://dblp.org/rec/bib/conf/lpar/2008},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@proceedings{DBLP:conf/cade/2007,
  editor    = {Frank Pfenning},
  title     = {Automated Deduction - CADE-21, 21st International Conference on Automated
               Deduction, Bremen, Germany, July 17-20, 2007, Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {4603},
  publisher = {Springer},
  year      = {2007},
  url       = {https://doi.org/10.1007/978-3-540-73595-3},
  doi       = {10.1007/978-3-540-73595-3},
  isbn      = {978-3-540-73594-6},
  timestamp = {Fri, 02 Jun 2017 13:01:06 +0200},
  biburl    = {https://dblp.org/rec/bib/conf/cade/2007},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@proceedings{DBLP:conf/cade/2007verify,
  editor    = {Bernhard Beckert},
  title     = {Proceedings of 4th International Verification Workshop in connection
               with CADE-21, Bremen, Germany, July 15-16, 2007},
  series    = {{CEUR} Workshop Proceedings},
  volume    = {259},
  publisher = {CEUR-WS.org},
  year      = {2007},
  url       = {http://ceur-ws.org/Vol-259},
  urn       = {urn:nbn:de:0074-259-9},
  timestamp = {Mon, 30 May 2016 16:57:34 +0200},
  biburl    = {https://dblp.org/rec/bib/conf/cade/2007verify},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@proceedings{DBLP:conf/cav/2007,
  editor    = {Werner Damm and
               Holger Hermanns},
  title     = {Computer Aided Verification, 19th International Conference, {CAV}
               2007, Berlin, Germany, July 3-7, 2007, Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {4590},
  publisher = {Springer},
  year      = {2007},
  url       = {https://doi.org/10.1007/978-3-540-73368-3},
  doi       = {10.1007/978-3-540-73368-3},
  isbn      = {978-3-540-73367-6},
  timestamp = {Fri, 02 Jun 2017 13:01:06 +0200},
  biburl    = {https://dblp.org/rec/bib/conf/cav/2007},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@proceedings{DBLP:conf/tableaux/2007,
  editor    = {Nicola Olivetti},
  title     = {Automated Reasoning with Analytic Tableaux and Related Methods, 16th
               International Conference, {TABLEAUX} 2007, Aix en Provence, France,
               July 3-6, 2007, Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {4548},
  publisher = {Springer},
  year      = {2007},
  url       = {https://doi.org/10.1007/978-3-540-73099-6},
  doi       = {10.1007/978-3-540-73099-6},
  isbn      = {978-3-540-73098-9},
  timestamp = {Fri, 02 Jun 2017 13:01:08 +0200},
  biburl    = {https://dblp.org/rec/bib/conf/tableaux/2007},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@proceedings{DBLP:conf/tacas/2007,
  editor    = {Orna Grumberg and
               Michael Huth},
  title     = {Tools and Algorithms for the Construction and Analysis of Systems,
               13th International Conference, {TACAS} 2007, Held as Part of the Joint
               European Conferences on Theory and Practice of Software, {ETAPS} 2007
               Braga, Portugal, March 24 - April 1, 2007, Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {4424},
  publisher = {Springer},
  year      = {2007},
  url       = {https://doi.org/10.1007/978-3-540-71209-1},
  doi       = {10.1007/978-3-540-71209-1},
  isbn      = {978-3-540-71208-4},
  timestamp = {Wed, 24 May 2017 08:28:32 +0200},
  biburl    = {https://dblp.org/rec/bib/conf/tacas/2007},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@proceedings{DBLP:conf/lpar/2006,
  editor    = {Miki Hermann and
               Andrei Voronkov},
  title     = {Logic for Programming, Artificial Intelligence, and Reasoning, 13th
               International Conference, {LPAR} 2006, Phnom Penh, Cambodia, November
               13-17, 2006, Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {4246},
  publisher = {Springer},
  year      = {2006},
  url       = {https://doi.org/10.1007/11916277},
  doi       = {10.1007/11916277},
  isbn      = {3-540-48281-4},
  timestamp = {Fri, 02 Jun 2017 13:01:08 +0200},
  biburl    = {https://dblp.org/rec/bib/conf/lpar/2006},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@proceedings{DBLP:conf/cade/2005,
  editor    = {Robert Nieuwenhuis},
  title     = {Automated Deduction - CADE-20, 20th International Conference on Automated
               Deduction, Tallinn, Estonia, July 22-27, 2005, Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {3632},
  publisher = {Springer},
  year      = {2005},
  url       = {https://doi.org/10.1007/11532231},
  doi       = {10.1007/11532231},
  isbn      = {3-540-28005-7},
  timestamp = {Tue, 30 May 2017 16:36:52 +0200},
  biburl    = {https://dblp.org/rec/bib/conf/cade/2005},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@proceedings{DBLP:conf/cade/2004,
  editor    = {David A. Basin and
               Micha{\"{e}}l Rusinowitch},
  title     = {Automated Reasoning - Second International Joint Conference, {IJCAR}
               2004, Cork, Ireland, July 4-8, 2004, Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {3097},
  publisher = {Springer},
  year      = {2004},
  url       = {https://doi.org/10.1007/b98691},
  doi       = {10.1007/b98691},
  isbn      = {3-540-22345-2},
  timestamp = {Tue, 30 May 2017 12:57:44 +0200},
  biburl    = {https://dblp.org/rec/bib/conf/cade/2004},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@proceedings{DBLP:conf/cav/2004,
  editor    = {Rajeev Alur and
               Doron A. Peled},
  title     = {Computer Aided Verification, 16th International Conference, {CAV}
               2004, Boston, MA, USA, July 13-17, 2004, Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {3114},
  publisher = {Springer},
  year      = {2004},
  url       = {https://doi.org/10.1007/b98490},
  doi       = {10.1007/b98490},
  isbn      = {3-540-22342-8},
  timestamp = {Tue, 30 May 2017 12:57:44 +0200},
  biburl    = {https://dblp.org/rec/bib/conf/cav/2004},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@proceedings{DBLP:conf/jelia/2004,
  editor    = {Jos{\'{e}} J{\'{u}}lio Alferes and
               Jo{\~{a}}o Alexandre Leite},
  title     = {Logics in Artificial Intelligence, 9th European Conference, {JELIA}
               2004, Lisbon, Portugal, September 27-30, 2004, Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {3229},
  publisher = {Springer},
  year      = {2004},
  url       = {https://doi.org/10.1007/b100483},
  doi       = {10.1007/b100483},
  isbn      = {3-540-23242-7},
  timestamp = {Tue, 30 May 2017 12:57:44 +0200},
  biburl    = {https://dblp.org/rec/bib/conf/jelia/2004},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@proceedings{DBLP:conf/lpar/2004,
  editor    = {Franz Baader and
               Andrei Voronkov},
  title     = {Logic for Programming, Artificial Intelligence, and Reasoning, 11th
               International Conference, {LPAR} 2004, Montevideo, Uruguay, March
               14-18, 2005, Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {3452},
  publisher = {Springer},
  year      = {2005},
  url       = {https://doi.org/10.1007/b106931},
  doi       = {10.1007/b106931},
  isbn      = {3-540-25236-3},
  timestamp = {Tue, 30 May 2017 16:36:53 +0200},
  biburl    = {https://dblp.org/rec/bib/conf/lpar/2004},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@proceedings{DBLP:conf/cade/2003,
  editor    = {Franz Baader},
  title     = {Automated Deduction - CADE-19, 19th International Conference on Automated
               Deduction Miami Beach, FL, USA, July 28 - August 2, 2003, Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {2741},
  publisher = {Springer},
  year      = {2003},
  url       = {https://doi.org/10.1007/b11829},
  doi       = {10.1007/b11829},
  isbn      = {3-540-40559-3},
  timestamp = {Mon, 29 May 2017 16:53:43 +0200},
  biburl    = {https://dblp.org/rec/bib/conf/cade/2003},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@proceedings{DBLP:conf/jelia/2002,
  editor    = {Sergio Flesca and
               Sergio Greco and
               Nicola Leone and
               Giovambattista Ianni},
  title     = {Logics in Artificial Intelligence, European Conference, {JELIA} 2002,
               Cosenza, Italy, September, 23-26, Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {2424},
  publisher = {Springer},
  year      = {2002},
  url       = {https://doi.org/10.1007/3-540-45757-7},
  doi       = {10.1007/3-540-45757-7},
  isbn      = {3-540-44190-5},
  timestamp = {Thu, 15 Jun 2017 21:42:21 +0200},
  biburl    = {https://dblp.org/rec/bib/conf/jelia/2002},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@proceedings{DBLP:conf/rta/2002,
  editor    = {Sophie Tison},
  title     = {Rewriting Techniques and Applications, 13th International Conference,
               {RTA} 2002, Copenhagen, Denmark, July 22-24, 2002, Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {2378},
  publisher = {Springer},
  year      = {2002},
  url       = {https://doi.org/10.1007/3-540-45610-4},
  doi       = {10.1007/3-540-45610-4},
  isbn      = {3-540-43916-1},
  timestamp = {Thu, 15 Jun 2017 21:39:22 +0200},
  biburl    = {https://dblp.org/rec/bib/conf/rta/2002},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@proceedings{DBLP:conf/frocos/2000,
  editor    = {H{\'{e}}l{\`{e}}ne Kirchner and
               Christophe Ringeissen},
  title     = {Frontiers of Combining Systems, Third International Workshop, FroCoS
               2000, Nancy, France, March 22-24, 2000, Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {1794},
  publisher = {Springer},
  year      = {2000},
  url       = {https://doi.org/10.1007/10720084},
  doi       = {10.1007/10720084},
  isbn      = {3-540-67281-8},
  timestamp = {Wed, 24 May 2017 15:40:45 +0200},
  biburl    = {https://dblp.org/rec/bib/conf/frocos/2000},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@proceedings{DBLP:conf/rta/1999,
  editor    = {Paliath Narendran and
               Micha{\"{e}}l Rusinowitch},
  title     = {Rewriting Techniques and Applications, 10th International Conference,
               RTA-99, Trento, Italy, July 2-4, 1999, Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {1631},
  publisher = {Springer},
  year      = {1999},
  url       = {https://doi.org/10.1007/3-540-48685-2},
  doi       = {10.1007/3-540-48685-2},
  isbn      = {3-540-66201-4},
  timestamp = {Wed, 24 May 2017 15:40:43 +0200},
  biburl    = {https://dblp.org/rec/bib/conf/rta/1999},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@proceedings{DBLP:conf/cade/1997,
  editor    = {William McCune},
  title     = {Automated Deduction - CADE-14, 14th International Conference on Automated
               Deduction, Townsville, North Queensland, Australia, July 13-17, 1997,
               Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {1249},
  publisher = {Springer},
  year      = {1997},
  url       = {https://doi.org/10.1007/3-540-63104-6},
  doi       = {10.1007/3-540-63104-6},
  isbn      = {3-540-63104-6},
  timestamp = {Mon, 22 May 2017 17:10:59 +0200},
  biburl    = {https://dblp.org/rec/bib/conf/cade/1997},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@proceedings{DBLP:conf/cp/1996,
  editor    = {Eugene C. Freuder},
  title     = {Proceedings of the Second International Conference on Principles and
               Practice of Constraint Programming, Cambridge, Massachusetts, USA,
               August 19-22, 1996},
  series    = {Lecture Notes in Computer Science},
  volume    = {1118},
  publisher = {Springer},
  year      = {1996},
  url       = {https://doi.org/10.1007/3-540-61551-2},
  doi       = {10.1007/3-540-61551-2},
  timestamp = {Mon, 22 May 2017 16:14:04 +0200},
  biburl    = {https://dblp.org/rec/bib/conf/cp/1996},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@proceedings{DBLP:conf/frocos/1996,
  editor    = {Franz Baader and
               Klaus U. Schulz},
  title     = {Frontiers of Combining Systems, First International Workshop FroCoS
               1996, Munich, Germany, March 26-29, 1996, Proceedings},
  series    = {Applied Logic Series},
  volume    = {3},
  publisher = {Kluwer Academic Publishers},
  year      = {1996},
  isbn      = {0-7923-4271-2},
  timestamp = {Mon, 20 Mar 2017 13:54:49 +0100},
  biburl    = {https://dblp.org/rec/bib/conf/frocos/1996},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
maintained by Schloss Dagstuhl LZI, founded at University of Trier