@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(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(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},
)
@inproceedings(DBLP:conf/atva/GurfinkelSV18,
 author       = {Arie Gurfinkel and Sharon Shoham and Yakir Vizel},
 year         = {2018},
 title        = {Quantifiers on Demand},
 editor       = {Shuvendu K. Lahiri and Chao Wang},
 booktitle    = {Automated Technology for Verification and Analysis - 16th International Symposium, {ATVA} 2018, Los Angeles, CA, USA, October 7-10, 2018, Proceedings},
 series       = {Lecture Notes in Computer Science},
 volume       = {11138},
 publisher    = {Springer},
 pages        = {248--266},
 doi          = {10.1007/978-3-030-01090-4\_15},
)
@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},
 booktitle    = {Theory and Applications of Satisfiability Testing - {SAT} 2016 - 19th International Conference, Bordeaux, France, July 5-8, 2016, Proceedings},
 series       = {Lecture Notes in Computer Science},
 volume       = {9710},
 publisher    = {Springer},
 pages        = {547--553},
 doi          = {10.1007/978-3-319-40970-2\_35},
)
@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, Los Angeles, CA, USA, July 21-24, 2020, Proceedings, Part {II}},
 series       = {Lecture Notes in Computer Science},
 volume       = {12225},
 publisher    = {Springer},
 pages        = {101--125},
 doi          = {10.1007/978-3-030-53291-8\_7},
)
@inproceedings(DBLP:conf/iccad/KFG20,
 author       = {Hari Govind V. K. and Grigory Fedyukovich and Arie Gurfinkel},
 year         = {2020},
 title        = {Word Level Property Directed Reachability},
 booktitle    = {{IEEE/ACM} International Conference On Computer Aided Design, {ICCAD} 2020, San Diego, CA, USA, November 2-5, 2020},
 publisher    = {{IEEE}},
 pages        = {107:1--107:9},
 doi          = {10.1145/3400302.3415708},
)
@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(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    = {{PLDI} '21: 42nd {ACM} {SIGPLAN} International Conference on Programming Language Design and Implementation, Virtual Event, Canada, June 20-25, 20211},
 publisher    = {{ACM}},
 pages        = {451--465},
 doi          = {10.1145/3453483.3454055},
)
@inproceedings(Kura2021,
 author       = {Satoshi Kura and Hiroshi Unno and Ichiro Hasuo},
 year         = {2021},
 title        = {Decision Tree Learning in CEGIS-Based Termination Analysis},
 booktitle    = {Computer Aided Verification - 33rd International Conference, {CAV} 2021, Virtual Event, July 20-23, 2021, Proceedings, Part {II}},
 series       = {Lecture Notes in Computer Science},
 volume       = {12760},
 publisher    = {Springer},
 pages        = {75--98},
 doi          = {10.1007/978-3-030-81688-9\_4},
)
@inproceedings(McMillan2006,
 author       = {Kenneth L. McMillan},
 year         = {2006},
 title        = {Lazy Abstraction with Interpolants},
 editor       = {Thomas Ball and Robert B. Jones},
 booktitle    = {Computer Aided Verification, 18th International Conference, {CAV} 2006, Seattle, WA, USA, August 17-20, 2006, Proceedings},
 series       = {Lecture Notes in Computer Science},
 volume       = {4144},
 publisher    = {Springer},
 pages        = {123--136},
 doi          = {10.1007/11817963\_14},
)
@inproceedings(reynolds2013finite,
 author       = {Andrew Reynolds and Cesare Tinelli and Amit Goel and Sava Krsti{\'c}},
 year         = {2013},
 title        = {{Finite model finding in SMT}},
 booktitle    = {International Conference on Computer Aided Verification},
 series       = {Lecture Notes in Computer Science},
 volume       = {8044},
 publisher    = {Springer},
 pages        = {640--655},
 doi          = {10.1007/978-3-642-39799-8\_42},
)
@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(DBLP:journals/corr/abs-2008-02939,
 author       = {Philipp R{\"{u}}mmer},
 year         = {2020},
 title        = {Competition Report: {CHC-COMP-20}},
 editor       = {Laurent Fribourg and Matthias Heizmann},
 booktitle    = {Proceedings 8th International Workshop on Verification and Program Transformation and 7th Workshop on Horn Clauses for Verification and Synthesis, VPT/HCVS@ETAPS 2020, Dublin, Ireland, 25-26th April 2020},
 series       = {{EPTCS}},
 volume       = {320},
 pages        = {197--219},
 doi          = {10.4204/EPTCS.320.15},
)
@inproceedings(Satake2020,
 author       = {Yuki Satake and Hiroshi Unno and Hinata Yanagi},
 year         = {2020},
 title        = {Probabilistic Inference for Predicate Constraint Satisfaction},
 booktitle    = {The Thirty-Fourth {AAAI} Conference on Artificial Intelligence, {AAAI} 2020, The Thirty-Second Innovative Applications of Artificial Intelligence Conference, {IAAI} 2020, The Tenth {AAAI} Symposium on Educational Advances in Artificial Intelligence, {EAAI} 2020, New York, NY, USA, February 7-12, 2020},
 publisher    = {{AAAI} Press},
 pages        = {1644--1651},
 doi          = {10.1609/aaai.v34i02.5526},
)
@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(Unno2021,
 author       = {Hiroshi Unno and Tachio Terauchi and Eric Koskinen},
 year         = {2021},
 title        = {Constraint-based Relational Verification},
 booktitle    = {Computer Aided Verification - 33rd International Conference, {CAV} 2021, Virtual Event, July 20-23, 2021, Proceedings, Part {I}},
 series       = {Lecture Notes in Computer Science},
 volume       = {12759},
 publisher    = {Springer},
 pages        = {742--766},
 doi          = {10.1007/978-3-030-81685-8\_35},
)