@book(DBLP:books/mit/AbelsonS96,
 author       = {Harold Abelson and Gerald J. Sussman},
 year         = {1996},
 title        = {Structure and Interpretation of Computer Programs, Second Edition},
 publisher    = {{MIT} Press},
)
@article(DBLP:journals/tcs/AfratiGT03,
 author       = {Foto N. Afrati and Manolis Gergatsoulis and Francesca Toni},
 year         = {2003},
 title        = {Linearisability on datalog programs},
 journal      = {Theor. Comput. Sci.},
 volume       = {308},
 number       = {1-3},
 pages        = {199--226},
 doi          = {10.1016/S0304-3975(02)00730-2},
)
@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(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    = {Conference Record of the Fourth {ACM} Symposium on Principles of Programming Languages, Los Angeles, California, USA, January 1977},
 publisher    = {{ACM}},
 pages        = {238--252},
 doi          = {10.1145/512950.512973},
 url          = {http://dl.acm.org/citation.cfm?id=512950},
)
@inproceedings(Cousot-Halbwachs-78,
 author       = {Patrick Cousot and Nicolas Halbwachs},
 year         = {1978},
 title        = {Automatic Discovery of Linear Restraints Among Variables of a Program},
 editor       = {Alfred V. Aho and Stephen N. Zilles and Thomas G. Szymanski},
 booktitle    = {Conference Record of the Fifth Annual {ACM} Symposium on Principles of Programming Languages, Tucson, Arizona, USA, January 1978},
 publisher    = {{ACM} Press},
 pages        = {84--96},
 doi          = {10.1145/512760.512770},
 url          = {http://dl.acm.org/citation.cfm?id=512760},
)
@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    = {Tools and Algorithms for the Construction and Analysis of Systems - 20th International Conference, {TACAS} 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, {ETAPS} 2014, Grenoble, France, April 5-13, 2014. Proceedings},
 series       = {Lecture Notes in Computer Science},
 volume       = {8413},
 publisher    = {Springer},
 pages        = {568--574},
 doi          = {10.1007/978-3-642-54862-8\_47},
)
@inproceedings(DBLP:conf/stacs/EsparzaKL07,
 author       = {Javier Esparza and Stefan Kiefer and Michael Luttenberger},
 year         = {2007},
 title        = {On Fixed Point Equations over Commutative Semirings},
 booktitle    = {{STACS} 2007, 24th Annual Symposium on Theoretical Aspects of Computer Science, Proceedings},
 series       = {LNCS},
 volume       = {4393},
 publisher    = {Springer},
 pages        = {296--307},
 doi          = {10.1007/978-3-540-70918-3\_26},
)
@inproceedings(esparzalata2014,
 author       = {Javier Esparza and Michael Luttenberger and Maximilian Schlund},
 year         = {2014},
 title        = {A Brief History of Strahler Numbers},
 booktitle    = {LATA$\tmspace+\medmuskip{.2222em}$'14, 8th Int.\ Conf. on Language and Automata Theory and Applications},
 series       = {LNCS},
 volume       = {8370},
 publisher    = {Springer},
 pages        = {1–13},
 doi          = {10.1007/978-3-319-04921-2\_1},
)
@inproceedings(Gallagher-Lafave-Dagstuhl,
 author       = {J. P. Gallagher and L. Lafave},
 year         = {1996},
 title        = {Regular Approximation of Computation Paths in Logic and Functional Languages},
 booktitle    = {Partial Evaluation},
 series       = {LNCS},
 volume       = {1110},
 publisher    = {Springer},
 pages        = {115--136},
 doi          = {10.1007/3-540-61580-6\_7},
)
@techreport(TR145RUC,
 author       = {John P. Gallagher and Mai Ajspur and Bishoksan Kafle},
 year         = {2014},
 title        = {{An Optimised Algorithm for Determinisation and Completion of Finite Tree Automata}},
 type         = {Technical Report},
 number       = {145},
 institution  = {Roskilde University, Denmark},
 note         = {Available from http://arxiv.org/pdf/1511.03595v1.pdf},
)
@inproceedings(tacas13,
 author       = {Pierre Ganty and Radu Iosif and Kone\v{c}n\'{y}, Filip},
 year         = {2013},
 title        = {Underapproximation of Procedure Summaries for Integer Programs},
 booktitle    = {TACAS$\tmspace+\medmuskip{.2222em}$'13: Proc.\ 19th Int.\ Conf.\ on Tools and Algorithms for the Construction and Analysis of Systems},
 series       = {LNCS},
 volume       = {7795},
 publisher    = {Springer},
 pages        = {247--261},
 doi          = {10.1007/978-3-642-36742-7\_18},
)
@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 {H}orn Clauses - (Competition Contribution)},
 editor       = {Cormac Flanagan and Barbara K{\"o}nig},
 booktitle    = {TACAS},
 series       = {LNCS},
 volume       = {7214},
 publisher    = {Springer},
 pages        = {549--551},
 doi          = {10.1007/978-3-642-28756-5\_46},
)
@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    = {{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},
)
@article(Gruska71b,
 author       = {Jozef Gruska},
 year         = {1971},
 title        = {A Few Remarks on the Index of Context-Free Grammars and Languages},
 journal      = {Information and Control},
 volume       = {19},
 number       = {3},
 pages        = {216--223},
 doi          = {10.1016/S0019-9958(71)90095-7},
)
@inproceedings(DBLP:conf/sas/HeizmannHP09,
 author       = {Matthias Heizmann and Jochen Hoenicke and Andreas Podelski},
 year         = {2009},
 title        = {Refinement of Trace Abstraction.},
 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/cav/HeizmannHP13,
 author       = {Matthias Heizmann and Jochen Hoenicke and Andreas Podelski},
 year         = {2013},
 title        = {Software Model Checking for People Who Love Automata},
 booktitle    = {Computer Aided Verification - 25th International Conference, {CAV} 2013, Saint Petersburg, Russia, July 13-19, 2013. Proceedings},
 series       = {LNCS},
 volume       = {8044},
 publisher    = {Springer},
 pages        = {36--52},
 doi          = {10.1007/978-3-642-39799-8\_2},
)
@inproceedings(DBLP:conf/sat/HoderB12,
 author       = {Krystof Hoder and Bj{\o}rner, Nikolaj},
 year         = {2012},
 title        = {Generalized Property Directed Reachability},
 editor       = {Alessandro Cimatti and Roberto Sebastiani},
 booktitle    = {Theory and Applications of Satisfiability Testing - {SAT} 2012 - 15th International Conference, Trento, Italy, June 17-20, 2012. Proceedings},
 series       = {Lecture Notes in Computer Science},
 volume       = {7317},
 publisher    = {Springer},
 pages        = {157--171},
 doi          = {10.1007/978-3-642-31612-8\_13},
)
@inproceedings(DBLP:conf/pepm/KafleG15,
 author       = {Bishoksan Kafle and John P. Gallagher},
 year         = {2015},
 title        = {Constraint Specialisation in Horn Clause Verification},
 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},
)
@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    = {Verification, Model Checking, and Abstract Interpretation - 16th International Conference, {VMCAI} 2015, Mumbai, India, January 12-14, 2015. Proceedings},
 series       = {LNCS},
 volume       = {8931},
 publisher    = {Springer},
 pages        = {209--226},
 doi          = {10.1007/978-3-662-46081-8\_12},
)
@article(DBLP:journals/corr/abs-1112-2864,
 author       = {Michael Luttenberger},
 year         = {2011},
 title        = {An Extension of Parikh's Theorem beyond Idempotence},
 journal      = {CoRR},
 volume       = {abs/1112.2864},
 url          = {http://arxiv.org/abs/1112.2864},
)
@article(Pettorossi-Proietti,
 author       = {Alberto Pettorossi and Maurizio Proietti},
 year         = {1999},
 title        = {Synthesis and Transformation of Logic Programs Using Unfold/Fold Proofs.},
 journal      = {J. Log. Program.},
 volume       = {41},
 number       = {2-3},
 pages        = {197--230},
 doi          = {10.1016/S0743-1066(99)00029-1},
)
@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       = {Lecture Notes in Computer Science},
 volume       = {440},
 publisher    = {Springer},
 pages        = {382--383},
 doi          = {10.1007/3-540-52753-2\_52},
)