@inproceedings(bmc,
 author       = {Armin Biere and Alessandro Cimatti and Edmund Clarke and Yunshan Zhu},
 year         = {1999},
 title        = {Symbolic Model Checking without BDDs},
 editor       = {W. Rance Cleaveland},
 booktitle    = {Tools and Algorithms for the Construction and Analysis of Systems},
 publisher    = {Springer Berlin Heidelberg},
 address      = {Berlin, Heidelberg},
 pages        = {193--207},
 doi          = {10.1007/3-540-49059-0_14},
)
@inproceedings(BjornerGMR15,
 author       = {Bj{\o}rner, Nikolaj and Arie Gurfinkel and Kenneth L. McMillan and Andrey Rybalchenko},
 year         = {2015},
 title        = {{Horn} Clause Solvers for Program Verification},
 booktitle    = {Fields of Logic and Computation {II} - Essays Dedicated to Yuri Gurevich on the Occasion of His 75th Birthday},
 pages        = {24--51},
 doi          = {10.1007/978-3-319-23534-9_2},
)
@inproceedings(Blicha2019,
 author       = {Martin Blicha and Antti E. J. Hyv{\"a}rinen and Kofro{\v{n}}, Jan and Natasha Sharygina},
 year         = {2019},
 title        = {Decomposing Farkas Interpolants},
 editor       = {Tom{\'a}{\v{s}} Vojnar and Lijun Zhang},
 booktitle    = {Tools and Algorithms for the Construction and Analysis of Systems},
 publisher    = {Springer International Publishing},
 address      = {Cham},
 pages        = {3--20},
 doi          = {10.1007/978-3-030-17462-0_1},
)
@inproceedings(Blicha2020,
 author       = {Martin Blicha and Antti E. J. Hyv{\"a}rinen and Matteo Marescotti and Natasha Sharygina},
 year         = {2020},
 title        = {A Cooperative Parallelization Approach for Property-Directed k-Induction},
 editor       = {Dirk Beyer and Damien Zufferey},
 booktitle    = {Verification, Model Checking, and Abstract Interpretation},
 publisher    = {Springer International Publishing},
 address      = {Cham},
 pages        = {270--292},
 doi          = {10.1007/978-3-030-39322-9_13},
)
@inproceedings(ic3,
 author       = {Aaron R. Bradley},
 year         = {2011},
 title        = {SAT-Based Model Checking without Unrolling},
 booktitle    = {{VMCAI}},
 series       = {LNCS},
 volume       = {6538},
 publisher    = {Springer},
 pages        = {70--87},
 doi          = {10.1007/978-3-642-18275-4_7},
)
@article(ic3ia,
 author       = {Alessandro Cimatti and Alberto Griggio and Sergio Mover and Stefano Tonetta},
 year         = {2016},
 title        = {Infinite-state invariant checking with {IC3} and predicate abstraction},
 journal      = {Formal Methods Syst. Des.},
 volume       = {49},
 number       = {3},
 pages        = {190--218},
 doi          = {10.1007/s10703-016-0257-4},
)
@inproceedings(mathsat5,
 author       = {Alessandro Cimatti and Alberto Griggio and Bastiaan Schaafsma and Roberto Sebastiani},
 year         = {2013},
 title        = {{The MathSAT5 SMT Solver}},
 editor       = {Nir Piterman and Scott Smolka},
 booktitle    = {Proceedings of TACAS},
 series       = {LNCS},
 volume       = {7795},
 publisher    = {Springer},
 doi          = {10.1007/978-3-642-36742-7_7},
)
@inproceedings(journals/corr/abs-1907-03998,
 author       = {Daniel Dietsch and Matthias Heizmann and Jochen Hoenicke and Alexander Nutz and Andreas Podelski},
 year         = {2019},
 title        = {Ultimate TreeAutomizer {(CHC-COMP} Tool Description)},
 booktitle    = {HCVS/PERR@ETAPS},
 series       = {{EPTCS}},
 volume       = {296},
 pages        = {42--47},
 doi          = {10.4204/EPTCS.296.7},
)
@inproceedings(Yices2014,
 author       = {Bruno Dutertre},
 year         = {2014},
 title        = {Yices 2.2},
 editor       = {Armin Biere and Roderick Bloem},
 booktitle    = {Computer-Aided Verification (CAV'2014)},
 series       = {LNCS},
 volume       = {8559},
 publisher    = {Springer},
 pages        = {737--744},
 doi          = {10.1007/978-3-319-08867-9_49},
)
@inproceedings(andrey-pldi,
 author       = {Sergey Grebenshchikov and Nuno P. Lopes and Corneliu Popeea and Andrey Rybalchenko},
 year         = {2012},
 title        = {Synthesizing Software Verifiers from Proof Rules},
 booktitle    = {PLDI},
 publisher    = {ACM},
 pages        = {405--416},
 doi          = {10.1145/2254064.2254112},
)
@article(ic3iacode,
 author       = {Alberto Griggio},
 year         = {Accessed 2020},
 title        = {Open-source IC3 Modulo Theories with Implicit Predicate Abstraction},
 url          = {https://es-static.fbk.eu/people/griggio/ic3ia/index.html},
)
@inproceedings(tacas/HeizmannCDGHLNM18,
 author       = {Matthias Heizmann and Yu{-}Fang Chen and Daniel Dietsch and Marius Greitschus and Jochen Hoenicke and Yong Li and Alexander Nutz and Betim Musa and Christian Schilling and Tanja Schindler and Andreas Podelski},
 year         = {2018},
 title        = {Ultimate Automizer and the Search for Perfect Interpolants - (Competition Contribution)},
 booktitle    = {{TACAS} {(2)}},
 series       = {LNCS},
 volume       = {10806},
 publisher    = {Springer},
 pages        = {447--451},
 doi          = {10.1007/978-3-319-89963-3_30},
)
@inproceedings(cav/HeizmannHP13,
 author       = {Matthias Heizmann and Jochen Hoenicke and Andreas Podelski},
 year         = {2013},
 title        = {Software Model Checking for People Who Love Automata},
 booktitle    = {{CAV}},
 series       = {LNCS},
 volume       = {8044},
 publisher    = {Springer},
 pages        = {36--52},
 doi          = {10.1007/978-3-642-39799-8_2},
)
@inproceedings(cade/HoenickeS18,
 author       = {Jochen Hoenicke and Tanja Schindler},
 year         = {2018},
 title        = {Efficient Interpolation for the Theory of Arrays},
 booktitle    = {{IJCAR}},
 series       = {LNCS},
 volume       = {10900},
 publisher    = {Springer},
 pages        = {549--565},
 doi          = {10.1007/978-3-319-94205-6_36},
)
@inproceedings(FMCAD2018HojjatRummer,
 author       = {Hossein Hojjat and Philipp R{\"{u}}mmer},
 year         = {2018},
 title        = {The {ELDARICA} Horn Solver},
 editor       = {Bj{\o}rner, Nikolaj and Arie Gurfinkel},
 booktitle    = {2018 Formal Methods in Computer Aided Design, {FMCAD}},
 publisher    = {{IEEE}},
 pages        = {1--7},
 doi          = {10.23919/FMCAD.2018.8603013},
)
@inproceedings(OpenSMT2,
 author       = {Antti E. J. Hyv{\"a}rinen and Matteo Marescotti and Leonardo Alt and Natasha Sharygina},
 year         = {2016},
 title        = {OpenSMT2: An SMT Solver for Multi-core and Cloud Computing},
 editor       = {Nadia Creignou and Le Berre, Daniel},
 booktitle    = {Theory and Applications of Satisfiability Testing -- SAT 2016},
 publisher    = {Springer International Publishing},
 address      = {Cham},
 pages        = {547--553},
 doi          = {10.1007/978-3-319-40970-2_35},
)
@inproceedings(Jovanovic2016,
 author       = {Dejan Jovanovi{\'c} and Bruno Dutertre},
 year         = {2016},
 title        = {Property-directed k-induction},
 booktitle    = {2016 Formal Methods in Computer-Aided Design (FMCAD)},
 pages        = {85--92},
 doi          = {10.1109/FMCAD.2016.7886665},
)
@inproceedings(gspc,
 author       = {Hari Govind V K and YuTing Chen and Sharon Shoham and Arie Gurfinkel},
 year         = {2020},
 title        = {Global Guidance for Local Generalization in Model Checking},
 booktitle    = {Computer Aided Verification - 32nd International Conference, {CAV} 2020},
 note         = {To appear},
)
@article(DBLP:journals/fmsd/KomuravelliGC16,
 author       = {Anvesh Komuravelli and Arie Gurfinkel and Sagar Chaki},
 year         = {2016},
 title        = {SMT-based model checking for recursive programs},
 journal      = {Formal Methods Syst. Des.},
 volume       = {48},
 number       = {3},
 pages        = {175--205},
 doi          = {10.1007/s10703-016-0249-4},
)
@inproceedings(cegar,
 author       = {Daniel Kroening and Alex Groce and Edmund M. Clarke},
 year         = {2004},
 title        = {Counterexample Guided Abstraction Refinement Via Program Execution},
 booktitle    = {{ICFEM}},
 series       = {LNCS},
 volume       = {3308},
 publisher    = {Springer},
 pages        = {224--238},
 doi          = {10.1007/978-3-540-30482-1_23},
)
@inproceedings(smts18,
 author       = {Matteo Marescotti and Hyv\textbackslash{}"arinen, Antti and Natasha Sharygina},
 year         = {2018},
 title        = {SMTS: Distributed, Visualized Constraint Solving},
 editor       = {Gilles Barthe and Geoff Sutcliffe and Margus Veanes},
 booktitle    = {LPAR-22. 22nd International Conference on Logic for Programming, Artificial Intelligence and Reasoning},
 series       = {EPiC Series in Computing},
 volume       = {57},
 publisher    = {EasyChair},
 pages        = {534--542},
 doi          = {10.29007/fhgn},
)
@inproceedings(princess08,
 author       = {Philipp R{\"u}mmer},
 year         = {2008},
 title        = {A Constraint Sequent Calculus for First-Order Logic with Linear Integer Arithmetic},
 booktitle    = {Proceedings, 15th International Conference on Logic for Programming, Artificial Intelligence and Reasoning},
 series       = {LNCS},
 volume       = {5330},
 publisher    = {Springer},
 pages        = {274--289},
 doi          = {10.1007/978-3-540-89439-1_20},
)
@inproceedings(Unno2020,
 author       = {Yuki Satake and Hiroshi Unno and Hinata Yanagi},
 year         = {2020},
 title        = {Probabilistic Inference for Predicate Constraint Satisfaction},
 booktitle    = {Proceedings of AAAI 2020},
 note         = {To appear},
)
@inproceedings(DBLP:conf/cade/StumpST14,
 author       = {Aaron Stump and Geoff Sutcliffe and Cesare Tinelli},
 year         = {2014},
 title        = {StarExec: {A} Cross-Community Infrastructure for Logic Solving},
 editor       = {St{\'{e}}phane Demri and Deepak Kapur and Christoph Weidenbach},
 booktitle    = {Automated Reasoning - 7th International Joint Conference, {IJCAR}},
 series       = {LNCS},
 volume       = {8562},
 publisher    = {Springer},
 pages        = {367--373},
 doi          = {10.1007/978-3-319-08587-6\_28},
)
@inproceedings(ToAppearZhangKong,
 author       = {Xiaozhen Zhang and Weiqiang Kong},
 year         = {2020},
 title        = {Facilitating CHC Solving with Improving Interpolation Abstraction Exploration},
 note         = {To appear},
)