@article(DBLP:journals/scp/BagnaraHZ08,
 author       = {Roberto Bagnara and Patricia M. Hill and Enea Zaffanella},
 year         = {2008},
 title        = {The Parma Polyhedra Library: Toward a complete set of numerical abstractions for the analysis and verification of hardware and software systems},
 journal      = {Sci. Comput. Program.},
 volume       = {72},
 number       = {1-2},
 pages        = {3--21},
 doi          = {10.1016/j.scico.2007.08.001},
)
@proceedings(DBLP:conf/tacas/2015,
 editor       = {Christel Baier and Cesare Tinelli},
 year         = {2015},
 title        = {{TACAS} . Proceedings},
 series       = {LNCS},
 volume       = {9035},
 publisher    = {Springer},
 doi          = {10.1007/978-3-662-46681-0},
)
@inproceedings(DBLP:conf/tacas/000115,
 author       = {Dirk Beyer},
 year         = {2015},
 title        = {Software Verification and Verifiable Witnesses - (Report on {SV-COMP} 2015)},
 editor       = {Baier and Tinelli},
 pages        = {401--416},
 doi          = {10.1007/978-3-662-46681-0\_31},
)
@proceedings(DBLP:journals/corr/BjornerFRS14,
 editor       = {Bj{\o}rner, Nikolaj and Fabio Fioravanti and Andrey Rybalchenko and Valerio Senni},
 year         = {2014},
 title        = {Proceedings First Workshop on {H}orn Clauses for Verification and Synthesis, {HCVS} 2014, Vienna, Austria, 17 July 2014},
 series       = {{EPTCS}},
 volume       = {169},
 doi          = {10.4204/EPTCS.169},
)
@inproceedings(DBLP:conf/birthday/BjornerGMR15,
 author       = {Bj{\o}rner, Nikolaj and Arie Gurfinkel and Kenneth L. McMillan and Andrey Rybalchenko},
 year         = {2015},
 title        = {{H}orn 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},
 series       = {{LNCS}},
 volume       = {9300},
 publisher    = {Springer},
 pages        = {24--51},
 doi          = {10.1007/978-3-319-23534-9\_2},
)
@inproceedings(DBLP:conf/sas/BjornerMR13,
 author       = {Bj{\o}rner, Nikolaj and Kenneth L. McMillan and Andrey Rybalchenko},
 year         = {2013},
 title        = {On Solving Universally Quantified {H}orn Clauses},
 editor       = {Francesco Logozzo and Manuel F{\"a}hndrich},
 booktitle    = {SAS},
 series       = {LNCS},
 volume       = {7935},
 publisher    = {Springer},
 pages        = {105--125},
 url          = {http://dx.doi.org/10.1007/978-3-642-38856-9_8},
)
@misc(Comon,
 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(Cousot-Halbwachs-78,
 author       = {P. Cousot and N. Halbwachs},
 year         = {{1978}},
 title        = {Automatic Discovery of Linear Restraints Among Variables of a Program},
 booktitle    = {Proceedings of the 5th Annual ACM Symposium on Principles of Programming Languages},
 pages        = {84--96},
 doi          = {10.1145/512760.512770},
)
@inproceedings(DBLP:conf/popl/CousotC77,
 author       = {Patrick Cousot and Radhia Cousot},
 year         = {1977},
 title        = {Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints},
 editor       = {Robert M. Graham and Michael A. Harrison and Ravi Sethi},
 booktitle    = {POPL},
 publisher    = {ACM},
 pages        = {238--252},
 url          = {http://doi.acm.org/10.1145/512950.512973},
)
@article(DBLP:journals/jsyml/Craig57,
 author       = {William Craig},
 year         = {1957},
 title        = {Linear Reasoning. {A} New Form of the Herbrand-Gentzen Theorem},
 journal      = {J. Symb. Log.},
 volume       = {22},
 number       = {3},
 pages        = {250--268},
 doi          = {10.2307/2963593},
)
@inproceedings(DBLP:conf/tacas/AngelisFPP14,
 author       = {De Angelis, Emanuele and Fabio Fioravanti and Alberto Pettorossi and Maurizio Proietti},
 year         = {2014},
 title        = {VeriMAP: A Tool for Verifying Programs through Transformations},
 editor       = {Erika {\'A}brah{\'a}m and Klaus Havelund},
 booktitle    = {TACAS},
 series       = {LNCS},
 volume       = {8413},
 publisher    = {Springer},
 pages        = {568--574},
 url          = {http://dx.doi.org/10.1007/978-3-642-54862-8_47},
)
@inproceedings(Dutertre:cav2014,
 author       = {Bruno Dutertre},
 year         = {2014},
 title        = {Yices 2.2},
 editor       = {Armin Biere and Roderick Bloem},
 booktitle    = {Computer-Aided Verification (CAV'2014)},
 series       = {Lecture Notes in Computer Science},
 volume       = {8559},
 publisher    = {Springer},
 pages        = {737--744},
 doi          = {10.1007/978-3-319-08867-9\_49},
)
@inproceedings(Gallagher-Lafave-Dagstuhl,
 author       = {J. P. Gallagher and L. Lafave},
 year         = {1996},
 title        = {Regular Approximation of Computation Paths in Logic and Functional Languages},
 editor       = {O. Danvy and R. Gl{\"u}ck and P. Thiemann},
 booktitle    = {Partial Evaluation},
 series       = {Springer-Verlag {LNCS}},
 volume       = {1110},
 pages        = {115--136},
 url          = {http://dx.doi.org/10.1007/3-540-61580-6\_7},
)
@article(DBLP:journals/corr/GallagherAK15,
 author       = {John P. Gallagher and Mai Ajspur and Bishoksan Kafle},
 year         = {2015},
 title        = {An Optimised Algorithm for Determinisation and Completion of Finite Tree Automata},
 journal      = {CoRR},
 volume       = {abs/1511.03595},
 url          = {http://arxiv.org/abs/1511.03595},
)
@article(DBLP:journals/corr/GallagherK14,
 author       = {John P. Gallagher and Bishoksan Kafle},
 year         = {2014},
 title        = {Analysis and Transformation Tools for Constrained {H}orn Clause Verification},
 journal      = {{TPLP}},
 volume       = {14},
 number       = {4-5 (additional materials in online edition)},
 pages        = {90--101},
 url          = {http://journals.cambridge.org/action/displaySuppMaterial?cupCode=1&type=4&jid=TLP&volumeId=14&issueId=4-5&aid=9303163},
)
@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},
 editor       = {Jan Vitek and Haibo Lin and Frank Tip},
 booktitle    = {{ACM} {SIGPLAN} Conference on Programming Language Design and Implementation, {PLDI} '12, Beijing, China - June 11 - 16, 2012},
 publisher    = {{ACM}},
 pages        = {405--416},
 doi          = {10.1145/2254064.2254112},
 url          = {http://dl.acm.org/citation.cfm?id=2254064},
)
@inproceedings(DBLP:conf/cav/GurfinkelKKN15,
 author       = {Arie Gurfinkel and Temesghen Kahsai and Anvesh Komuravelli and Jorge A. Navas},
 year         = {2015},
 title        = {The Sea{H}orn Verification Framework},
 editor       = {Daniel Kroening and Corina S. Pasareanu},
 booktitle    = {{CAV} , Proceedings, Part {I}},
 series       = {{LNCS}},
 volume       = {9206},
 publisher    = {Springer},
 pages        = {343--361},
 doi          = {10.1007/978-3-319-21690-4\_20},
)
@inproceedings(DBLP:conf/tacas/GurfinkelKN15,
 author       = {Arie Gurfinkel and Temesghen Kahsai and Jorge A. Navas},
 year         = {2015},
 title        = {Sea{H}orn: {A} Framework for Verifying {C} Programs (Competition Contribution)},
 editor       = {Baier and Tinelli},
 pages        = {447--450},
 doi          = {10.1007/978-3-662-46681-0\_41},
)
@inproceedings(DBLP:conf/sas/HeizmannHP09,
 author       = {Matthias Heizmann and Jochen Hoenicke and Andreas Podelski},
 year         = {2009},
 title        = {Refinement of Trace Abstraction.},
 editor       = {Jens Palsberg and Zhendong Su},
 booktitle    = {Static Analysis, 16th International Symposium, {SAS} 2009},
 series       = {LNCS},
 volume       = {5673},
 publisher    = {Springer},
 pages        = {69--85},
 doi          = {10.1007/978-3-642-03237-0\_7},
)
@inproceedings(DBLP:conf/popl/HeizmannHP10,
 author       = {Matthias Heizmann and Jochen Hoenicke and Andreas Podelski},
 year         = {2010},
 title        = {Nested interpolants},
 editor       = {Manuel V. Hermenegildo and Jens Palsberg},
 booktitle    = {Proceedings of the 37th {ACM} {SIGPLAN-SIGACT} Symposium on Principles of Programming Languages, {POPL} 2010, Madrid, Spain, January 17-23, 2010},
 publisher    = {{ACM}},
 pages        = {471--482},
 doi          = {10.1145/1706299.1706353},
 url          = {http://dl.acm.org/citation.cfm?id=1706299},
)
@inproceedings(DBLP:conf/cav/HeizmannHP13,
 author       = {Matthias Heizmann and Jochen Hoenicke and Andreas Podelski},
 year         = {2013},
 title        = {Software Model Checking for People Who Love Automata},
 editor       = {Sharygina and Veith},
 pages        = {36--52},
 doi          = {10.1007/978-3-642-39799-8\_2},
)
@article(DBLP:journals/tplp/HermenegildoBCLMMP12,
 author       = {Manuel V. Hermenegildo and Francisco Bueno and Manuel Carro and L{\'{o}}pez{-}Garc{\'{\i}}a, Pedro and Edison Mera and Jos{\'{e}} F. Morales and Germ{\'{a}}n Puebla},
 year         = {2012},
 title        = {An overview of Ciao and its design philosophy},
 journal      = {{TPLP}},
 volume       = {12},
 number       = {1-2},
 pages        = {219--252},
 doi          = {10.1017/S1471068411000457},
)
@inproceedings(DBLP:conf/fm/HojjatKGIKR12,
 author       = {Hossein Hojjat and Filip Konecn{\'{y}} and Florent Garnier and Radu Iosif and Viktor Kuncak and Philipp R{\"{u}}mmer},
 year         = {2012},
 title        = {A Verification Toolkit for Numerical Transition Systems - Tool Paper},
 editor       = {Dimitra Giannakopoulou and Dominique M{\'{e}}ry},
 booktitle    = {{FM} 2012: Formal Methods - 18th International Symposium, Paris, France, August 27-31, 2012. Proceedings},
 series       = {{LNCS}},
 volume       = {7436},
 publisher    = {Springer},
 pages        = {247--251},
 doi          = {10.1007/978-3-642-32759-9\_21},
)
@inproceedings(DBLP:conf/cav/JaffarMNS12,
 author       = {Joxan Jaffar and Vijayaraghavan Murali and Jorge A. Navas and Andrew E. Santosa},
 year         = {2012},
 title        = {TRACER: A Symbolic Execution Tool for Verification},
 editor       = {P. Madhusudan and Sanjit A. Seshia},
 booktitle    = {CAV},
 series       = {LNCS},
 volume       = {7358},
 publisher    = {Springer},
 pages        = {758--766},
 url          = {http://dx.doi.org/10.1007/978-3-642-31424-7_61},
)
@inproceedings(DBLP:conf/tacas/JhalaM06,
 author       = {Ranjit Jhala and Kenneth L. McMillan},
 year         = {2006},
 title        = {A Practical and Complete Approach to Predicate Refinement},
 editor       = {Holger Hermanns and Jens Palsberg},
 booktitle    = {TACAS},
 series       = {LNCS},
 volume       = {3920},
 publisher    = {Springer},
 pages        = {459--473},
 url          = {http://dx.doi.org/10.1007/11691372_33},
)
@inproceedings(DBLP:conf/pepm/KafleG15,
 author       = {Bishoksan Kafle and John P. Gallagher},
 year         = {2015},
 title        = {Constraint Specialisation in {H}orn Clause Verification},
 editor       = {Kenichi Asai and Kostis Sagonas},
 booktitle    = {Proceedings of the 2015 Workshop on Partial Evaluation and Program Manipulation, PEPM, Mumbai, India, January 15-17, 2015},
 publisher    = {{ACM}},
 pages        = {85--90},
 doi          = {10.1145/2678015.2682544},
 url          = {http://dl.acm.org/citation.cfm?id=2678015},
)
@article(kafleG2015horn,
 author       = {Bishoksan Kafle and John P. Gallagher},
 year         = {2015},
 title        = {{H}orn clause verification with convex polyhedral abstraction and tree automata-based refinement},
 journal      = {Computer Languages, Systems \& Structures},
 doi          = {10.1016/j.cl.2015.11.001},
)
@techreport(McmillanR2013,
 author       = {Kenneth L. McMillan and Andrey Rybalchenko},
 year         = {2013},
 title        = {Solving Constrained {H}orn Clauses using Interpolation},
 type         = {Technical Report},
 institution  = {Microsoft Research},
)
@inproceedings(DBLP:conf/cav/RummerHK13,
 author       = {Philipp R{\"u}mmer and Hossein Hojjat and Viktor Kuncak},
 year         = {2013},
 title        = {Disjunctive Interpolants for {H}orn-Clause Verification},
 editor       = {Sharygina and Veith},
 pages        = {347--363},
 doi          = {10.1007/978-3-642-39799-8\_24},
)
@article(DBLP:journals/jsc/RybalchenkoS10,
 author       = {Andrey Rybalchenko and Sofronie-Stokkermans, Viorica},
 year         = {2010},
 title        = {Constraint solving for interpolation},
 journal      = {J. Symb. Comput.},
 volume       = {45},
 number       = {11},
 pages        = {1212--1233},
 url          = {http://dx.doi.org/10.1016/j.jsc.2010.06.005},
)
@proceedings(DBLP:conf/cav/2013,
 editor       = {Natasha Sharygina and Helmut Veith},
 year         = {2013},
 title        = {Computer Aided Verification - 25th International Conference, {CAV} 2013, Saint Petersburg, Russia, July 13-19, 2013. Proceedings},
 series       = {{LNCS}},
 volume       = {8044},
 publisher    = {Springer},
 doi          = {10.1007/978-3-642-39799-8},
)
@inproceedings(Stark89,
 author       = {Robert F. St{\"a}rk},
 year         = {1989},
 title        = {A Direct Proof for the Completeness of {SLD}-Resolution},
 editor       = {Egon B{\"o}rger and Hans Kleine B{\"u}ning and Michael M. Richter},
 booktitle    = {CSL '89, 3rd Workshop on Computer Science Logic, Kaiserslautern, Germany, October 2-6, 1989, Proceedings},
 series       = {LNCS},
 volume       = {440},
 publisher    = {Springer},
 pages        = {382--383},
)
@techreport(WangJ2015,
 author       = {Weifeng Wang and Li Jiao},
 year         = {2015},
 title        = {Trace abstraction refinement for solving {H}orn clauses},
 type         = {Technical Report},
 number       = {ISCAS-SKLCS-15-19},
 institution  = {State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences},
 note         = {Available on: \url{http://lcs.ios.ac.cn/~wangwf/TechReportISCAS-SKLCS-15-19.pdf}},
)