@inproceedings(DBLP:conf/wia/AbdullaKH06,
 author       = {Parosh Aziz Abdulla and Lisa Kaati and Johanna H{\"{o}}gberg},
 year         = {2006},
 title        = {Bisimulation Minimization of Tree Automata},
 booktitle    = {{CIAA}},
 series       = {Lecture Notes in Computer Science},
 volume       = {4094},
 publisher    = {Springer},
 pages        = {173--185},
 doi          = {10.1137/0216062},
)
@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},
 year         = {2011},
 title        = {{CVC4}},
 booktitle    = {{CAV}},
 series       = {Lecture Notes in Computer Science},
 volume       = {6806},
 publisher    = {Springer},
 pages        = {171--177},
 doi          = {10.1007/3-540-45657-0_40},
)
@inproceedings(DBLP:conf/birthday/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}},
 series       = {Lecture Notes in Computer Science},
 volume       = {9300},
 publisher    = {Springer},
 pages        = {24--51},
 doi          = {10.1007/978-3-319-19249-9},
)
@inproceedings(DBLP:conf/spin/ChristHN12,
 author       = {J{\"{u}}rgen Christ and Jochen Hoenicke and Alexander Nutz},
 year         = {2012},
 title        = {SMTInterpol: An Interpolating {SMT} Solver},
 booktitle    = {{SPIN}},
 series       = {Lecture Notes in Computer Science},
 volume       = {7385},
 publisher    = {Springer},
 pages        = {248--254},
 doi          = {10.1007/11532231_26},
)
@inproceedings(DBLP:conf/tacas/CimattiGSS13,
 author       = {Alessandro Cimatti and Alberto Griggio and Bastiaan Joost Schaafsma and Roberto Sebastiani},
 year         = {2013},
 title        = {The MathSAT5 {SMT} Solver},
 booktitle    = {{TACAS}},
 series       = {Lecture Notes in Computer Science},
 volume       = {7795},
 publisher    = {Springer},
 pages        = {93--107},
 doi          = {10.1007/978-3-642-31365-3_38},
)
@inproceedings(DBLP:conf/cav/ClarkeGJLV00,
 author       = {Edmund M. Clarke and Orna Grumberg and Somesh Jha and Yuan Lu and Helmut Veith},
 year         = {2000},
 title        = {Counterexample-Guided Abstraction Refinement},
 booktitle    = {{CAV}},
 series       = {Lecture Notes in Computer Science},
 volume       = {1855},
 publisher    = {Springer},
 pages        = {154--169},
 doi          = {10.1007/3-540-49519-3_18},
)
@misc(tata2007,
 author       = {H. Comon and M. Dauchet and R. Gilleron and C. L\"oding and F. Jacquemard and D. Lugiez and S. Tison and M. Tommasi},
 year         = {2007},
 title        = {Tree Automata Techniques and Applications},
 howpublished = {Available on: \url{http://www.grappa.univ-lille3.fr/tata}},
 note         = {Release October, 12th 2007},
)
@inproceedings(DBLP:conf/sigsoft/DietschHMNP17,
 author       = {Daniel Dietsch and Matthias Heizmann and Betim Musa and Alexander Nutz and Andreas Podelski},
 year         = {2017},
 title        = {Craig vs. Newton in software model checking},
 booktitle    = {{ESEC/SIGSOFT} {FSE}},
 publisher    = {{ACM}},
 pages        = {487--497},
 doi          = {10.1145/3106237.3106307},
)
@inproceedings(DBLP:conf/fmcad/EenMB11,
 author       = {Niklas E{\'{e}}n and Alan Mishchenko and Robert K. Brayton},
 year         = {2011},
 title        = {Efficient implementation of property directed reachability},
 booktitle    = {{FMCAD}},
 publisher    = {{FMCAD} Inc.},
 pages        = {125--134},
)
@inproceedings(DBLP:conf/tacas/GrebenshchikovGLPR12,
 author       = {Sergey Grebenshchikov and Ashutosh Gupta and Nuno P. Lopes and Corneliu Popeea and Andrey Rybalchenko},
 year         = {2012},
 title        = {{HSF(C):} {A} Software Verifier Based on Horn Clauses - (Competition Contribution)},
 booktitle    = {{TACAS}},
 series       = {Lecture Notes in Computer Science},
 volume       = {7214},
 publisher    = {Springer},
 pages        = {549--551},
 doi          = {10.1007/978-3-540-69611-7_16},
)
@inproceedings(DBLP:conf/pldi/GrebenshchikovLPR12,
 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/sas/HeizmannHP09,
 author       = {Matthias Heizmann and Jochen Hoenicke and Andreas Podelski},
 year         = {2009},
 title        = {Refinement of Trace Abstraction},
 booktitle    = {{SAS}},
 series       = {Lecture Notes in Computer Science},
 volume       = {5673},
 publisher    = {Springer},
 pages        = {69--85},
 doi          = {10.1007/978-3-540-73368-3_46},
)
@inproceedings(DBLP:conf/popl/HeizmannHP10,
 author       = {Matthias Heizmann and Jochen Hoenicke and Andreas Podelski},
 year         = {2010},
 title        = {Nested interpolants},
 booktitle    = {{POPL}},
 publisher    = {{ACM}},
 pages        = {471--482},
 doi          = {10.1145/1706299.1706353},
)
@inproceedings(DBLP:conf/sat/HoderB12,
 author       = {Krystof Hoder and Bj{\o}rner, Nikolaj},
 year         = {2012},
 title        = {Generalized Property Directed Reachability},
 booktitle    = {{SAT}},
 series       = {Lecture Notes in Computer Science},
 volume       = {7317},
 publisher    = {Springer},
 pages        = {157--171},
 doi          = {10.1007/3-540-49481-2_26},
)
@inproceedings(DBLP:conf/popl/HoenickeMP17,
 author       = {Jochen Hoenicke and Rupak Majumdar and Andreas Podelski},
 year         = {2017},
 title        = {Thread modularity at many levels: a pearl in compositional verification},
 booktitle    = {{POPL}},
 publisher    = {{ACM}},
 pages        = {473--485},
 doi          = {10.1145/3009837.3009893},
)
@inproceedings(DBLP:conf/vmcai/KafleG15,
 author       = {Bishoksan Kafle and John P. Gallagher},
 year         = {2015},
 title        = {Tree Automata-Based Refinement with Application to Horn Clause Verification},
 booktitle    = {{VMCAI}},
 series       = {Lecture Notes in Computer Science},
 volume       = {8931},
 publisher    = {Springer},
 pages        = {209--226},
 doi          = {10.1007/3-540-52753-2_52},
)
@inproceedings(DBLP:conf/cav/KafleGM16,
 author       = {Bishoksan Kafle and John P. Gallagher and Jos{\'{e}} F. Morales},
 year         = {2016},
 title        = {Rahft: {A} Tool for Verifying Horn Clauses Using Abstract Interpretation and Finite Tree Automata},
 booktitle    = {{CAV} {(1)}},
 series       = {Lecture Notes in Computer Science},
 volume       = {9779},
 publisher    = {Springer},
 pages        = {261--268},
 doi          = {10.1016/j.jsc.2010.06.005},
)
@inproceedings(DBLP:conf/tacas/MouraB08,
 author       = {Leonardo Mendon{\c{c}}a de Moura and Bj{\o}rner, Nikolaj},
 year         = {2008},
 title        = {{Z3:} An Efficient {SMT} Solver},
 booktitle    = {{TACAS}},
 series       = {Lecture Notes in Computer Science},
 volume       = {4963},
 publisher    = {Springer},
 pages        = {337--340},
 doi          = {10.1109/MS.2006.117},
)
@article(DBLP:journals/cj/WangJ16,
 author       = {Weifeng Wang and Li Jiao},
 year         = {2016},
 title        = {Trace Abstraction Refinement for Solving Horn Clauses},
 journal      = {Comput. J.},
 volume       = {59},
 number       = {8},
 pages        = {1236--1251},
 doi          = {10.1145/69575.69577},
)