@misc(BarFT-SMTLIB,
 author       = {Clark Barrett and Pascal Fontaine and Cesare Tinelli},
 year         = {2016},
 title        = {{The Satisfiability Modulo Theories Library (SMT-LIB)}},
 howpublished = {{\tt www.SMT-LIB.org}},
)
@incollection(BGMR2015,
 author       = {Bj{\o}rner, Nikolaj and Arie Gurfinkel and Ken McMillan and Andrey Rybalchenko},
 year         = {2015},
 title        = {Horn Clause Solvers for Program Verification},
 editor       = {Lev D. Beklemishev and Andreas Blass and Nachum Dershowitz and Bernd Finkbeiner and Wolfram Schulte},
 booktitle    = {Fields of Logic and Computation II: Essays Dedicated to Yuri Gurevich on the Occasion of His 75th Birthday},
 publisher    = {Springer International Publishing},
 address      = {Cham},
 pages        = {24--51},
 doi          = {10.1007/978-3-319-23534-9\_2},
)
@inproceedings(Blicha_2022,
 author       = {Martin Blicha and Grigory Fedyukovich and Antti E. J. Hyv{\"a}rinen and Natasha Sharygina},
 year         = {2022},
 title        = {Transition Power Abstractions for Deep Counterexample Detection},
 editor       = {Dana Fisman and Grigore Rosu},
 booktitle    = {Tools and Algorithms for the Construction and Analysis of Systems},
 publisher    = {Springer International Publishing},
 address      = {Cham},
 pages        = {524--542},
 doi          = {10.1007/978-3-030-99524-9\_29},
)
@article(DFGHPP2021,
 author       = {De Angelis, Emanuele and Fabio Fioravanti and John P. Gallagher and Manuel V. Hermenegildo and Alberto Pettorossi and Maurizio Proeitti},
 year         = {2021},
 title        = {Analysis and Transformation of Constrained Horn Clauses for Program Verification},
 journal      = {Theory and Practice of Logic Programming},
 pages        = {1--69},
 doi          = {10.1017/S1471068421000211},
)
@article(DBLP:journals/logcom/AngelisFPP22,
 author       = {{De Angelis}, Emanuele and Fabio Fioravanti and Alberto Pettorossi and Maurizio Proietti},
 year         = {2022},
 title        = {Satisfiability of constrained Horn clauses on algebraic data types: {A} transformation-based approach},
 journal      = {J. Log. Comput.},
 volume       = {32},
 number       = {2},
 pages        = {402--442},
 doi          = {10.1093/logcom/exab090},
)
@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(chccomp21,
 author       = {Grigory Fedyukovich and Philipp R{\"{u}}mmer},
 year         = {2021},
 title        = {Competition Report: {CHC-COMP-21}},
 editor       = {Hossein Hojjat and Bishoksan Kafle},
 booktitle    = {Proceedings 8th Workshop on Horn Clauses for Verification and Synthesis, HCVS@ETAPS 2021, Virtual, 28th March 2021},
 series       = {{EPTCS}},
 volume       = {344},
 publisher    = {Open Publishing Association},
 pages        = {91--108},
 doi          = {10.4204/EPTCS.344.7},
)
@inproceedings(Gurfinkel2022,
 author       = {Arie Gurfinkel},
 year         = {2022},
 title        = {Program Verification with Constrained Horn Clauses (Invited Paper)},
 editor       = {Sharon Shoham and Yakir Vizel},
 booktitle    = {Computer Aided Verification},
 publisher    = {Springer International Publishing},
 address      = {Cham},
 pages        = {19--29},
 doi          = {10.1007/978-3-031-13185-1\_2},
)
@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       = {Lecture Notes in Computer Science},
 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       = {Lecture Notes in Computer Science},
 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       = {Lecture Notes in Computer Science},
 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},
 booktitle    = {2018 Formal Methods in Computer Aided Design, {FMCAD}},
 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},
)
@article(DBLP:journals/pacmpl/KSG22,
 author       = {Hari Govind V. K. and Sharon Shoham and Arie Gurfinkel},
 year         = {2022},
 title        = {Solving constrained Horn clauses modulo algebraic data types and recursive functions},
 journal      = {Proc. {ACM} Program. Lang.},
 volume       = {6},
 number       = {{POPL}},
 pages        = {1--29},
 doi          = {10.1145/3498722},
)
@article(Komuravelli2016,
 author       = {Anvesh Komuravelli and Arie Gurfinkel and Sagar Chaki},
 year         = {2016},
 title        = {{SMT}-based Model Checking For Recursive Programs},
 journal      = {Formal Methods in System Design},
 volume       = {48},
 number       = {3},
 pages        = {175--205},
 doi          = {10.1007/s10703-016-0249-4},
)
@inproceedings(kostyukov2021finite,
 author       = {Yurii Kostyukov and Dmitry Mordvinov and Grigory Fedyukovich},
 year         = {2021},
 title        = {Beyond the Elementary Representations of Program Invariants over Algebraic Data Types},
 booktitle    = {Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation},
 series       = {PLDI 2021},
 publisher    = {{ACM}},
 pages        = {451--465},
 doi          = {10.1145/3453483.3454055},
)
@inproceedings(McMillan_2006,
 author       = {Kenneth L. McMillan},
 year         = {2006},
 title        = {Lazy Abstraction with Interpolants},
 editor       = {Thomas Ball and Robert B. Jones},
 booktitle    = {Computer Aided Verification},
 publisher    = {Springer Berlin Heidelberg},
 address      = {Berlin, Heidelberg},
 pages        = {123--136},
 doi          = {10.1007/11817963\_14},
)
@article(vampire,
 author       = {Alexandre Riazanov and Andrei Voronkov},
 year         = {2002},
 title        = {The Design and Implementation of VAMPIRE},
 journal      = {AI Commun.},
 volume       = {15},
 number       = {2,3},
 pages        = {91--110},
)
@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(starexec,
 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},
 publisher    = {Springer International Publishing},
 address      = {Cham},
 pages        = {367--373},
 doi          = {10.1007/978-3-319-08587-6\_28},
)