@incollection(BaS01,
 author       = {F. Baader and W. Snyder},
 year         = {2001},
 title        = {Unification Theory},
 editor       = {A. Robinson and A. Voronkov},
 booktitle    = {Handbook of Automated Reasoning},
 volume       = {I},
 publisher    = {Elsevier Science},
 pages        = {445--532},
 doi          = {10.1016/B978-044450813-3/50010-2},
)
@inproceedings(Bra11,
 author       = {A. R. Bradley},
 year         = {2011},
 title        = {{SAT}-Based Model Checking without Unrolling},
 editor       = {Ranjit Jhala and David A. Schmidt},
 booktitle    = {Verification, Model Checking, and Abstract Interpretation - 12th International Conference, {VMCAI} 2011, Austin, TX, USA, January 23--25, 2011. Proceedings},
 series       = {Lecture Notes in Computer Science 6538},
 publisher    = {Springer},
 pages        = {70--87},
 doi          = {10.1007/978-3-642-18275-4_7},
)
@incollection(Bun01,
 author       = {A. Bundy},
 year         = {2001},
 title        = {The Automation of Proof by Mathematical Induction},
 editor       = {A. Robinson and A. Voronkov},
 booktitle    = {Handbook of Automated Reasoning},
 volume       = {I},
 publisher    = {North Holland},
 pages        = {845--911},
 doi          = {10.1016/B978-044450813-3/50015-1},
)
@inproceedings(Cl&00,
 author       = {E.M. Clarke and O. Grumberg and S. Jha and Y. Lu and H. Veith},
 year         = {2000},
 title        = {{C}ounterexample-{G}uided {A}bstraction {R}efinement},
 editor       = {E.A. Emerson and A.P. Sistla},
 booktitle    = {Proceedings of the 12th International Conference on {C}omputer {A}ided {V}erification, CAV~'00},
 series       = {Lecture Notes in Computer Science 1855},
 publisher    = {Springer},
 pages        = {154--169},
 doi          = {10.1007/10722167_15},
)
@article(De&14c,
 author       = {{De Angelis}, E. and F. Fioravanti and A. Pettorossi and M. Proietti},
 year         = {2014},
 title        = {Program Verification via Iterated Specialization},
 journal      = {Science of Computer Programming},
 volume       = {95, Part 2},
 pages        = {149--175},
 doi          = {10.1016/j.scico.2014.05.017},
 note         = {Selected and extended papers from Partial Evaluation and Program Manipulation 2013},
)
@inproceedings(De&14b,
 author       = {{De Angelis}, E. and F. Fioravanti and A. Pettorossi and M. Proietti},
 year         = {2014},
 title        = {{V}eri{MAP}: {A} {T}ool for {V}erifying {P}rograms through {T}ransformations},
 editor       = {E. \'{A}brah\'{a}m and K. Havelund},
 booktitle    = {Proceedings of the 20th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS~'14},
 series       = {Lecture Notes in Computer Science 8413},
 publisher    = {Springer},
 pages        = {568--574},
 doi          = {10.1007/978-3-642-54862-8_47},
 note         = {Available at: {\tt http://www.map.uniroma2.it/VeriMAP}},
)
@article(De&15c,
 author       = {{De Angelis}, E. and F. Fioravanti and A. Pettorossi and M. Proietti},
 year         = {2015},
 title        = {Proving correctness of imperative programs by linearizing constrained {H}orn clauses},
 journal      = {Theory and Practice of Logic Programming},
 volume       = {15},
 number       = {4--5},
 pages        = {635--650},
 doi          = {10.1017/S1471068415000289},
)
@article(De&17b,
 author       = {{De Angelis}, E. and F. Fioravanti and A. Pettorossi and M. Proietti},
 year         = {2017},
 title        = {Semantics-based generation of verification conditions via program specialization},
 journal      = {Science of Computer Programming},
 volume       = {147},
 pages        = {78--108},
 doi          = {10.1016/j.scico.2016.11.002},
 note         = {Selected and Extended papers from the International Symposium on Principles and Practice of Declarative Programming 2015},
)
@article(De&18c,
 author       = {{De Angelis}, E. and F. Fioravanti and A. Pettorossi and M. Proietti},
 year         = {2018},
 title        = {Predicate Pairing for program verification},
 journal      = {{TPLP}},
 volume       = {18},
 number       = {2},
 pages        = {126--166},
 doi          = {10.1017/S1471068417000497},
)
@article(De&18a,
 author       = {{De Angelis}, E. and F. Fioravanti and A. Pettorossi and M. Proietti},
 year         = {2018},
 title        = {Solving Horn Clauses on Inductive Data Types Without Induction},
 journal      = {{TPLP}},
 volume       = {18},
 number       = {3-4},
 pages        = {452--469},
 doi          = {10.1017/S1471068418000157},
)
@inproceedings(De&19b,
 author       = {{De Angelis}, E. and F. Fioravanti and A. Pettorossi and M. Proietti},
 year         = {2019},
 title        = {Proving Properties of Sorting Programs: {A} Case Study in {H}orn Clause Verification},
 editor       = {E. De Angelis and G. Fedyukovich and N. Tzevelekos and M. Ulbrich},
 booktitle    = {Proceedings of {HCVS/PERR 2019}: 6th Workshop on Horn Clauses for Verification and Synthesis and 3rd Workshop on Program Equivalence and Relational Reasoning, Prague, Czech Republic, April 6--7, 2019},
 series       = {To appear in EPTCS},
 url          = {https://conf.researchr.org/details/etaps-2019/hcvs-2019-papers/3/Proving-Properties-of-Sorting-Programs-A-Case-Study-in-Horn-Clause-Verification},
)
@article(EtG96,
 author       = {S. Etalle and M. Gabbrielli},
 year         = {1996},
 title        = {Trans\-form\-ations of {CLP} Modules},
 journal      = {Theoretical Computer Science},
 volume       = {166},
 pages        = {101--146},
 doi          = {10.1016/0304-3975(95)00148-4},
)
@inproceedings(Gr&12,
 author       = {S. Grebenshchikov and N. P. Lopes and C. Popeea and A. Rybalchenko},
 year         = {2012},
 title        = {Synthesizing software verifiers from proof rules},
 booktitle    = {Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI~'12},
 pages        = {405--416},
 doi          = {10.1145/2345156.2254112},
)
@inproceedings(HoB12,
 author       = {K. Hoder and Bj{\o}rner, N.},
 year         = {2012},
 title        = {Generalized Property Directed Reachability},
 editor       = {Alessandro Cimatti and Roberto Sebastiani},
 booktitle    = {Proceedings of the 15th International Conference on Theory and Applications of Satisfiability Testing, SAT '12},
 series       = {Lecture Notes in Computer Science 7317},
 publisher    = {Springer},
 address      = {Berlin, Heidelberg},
 pages        = {157--171},
 doi          = {10.1007/978-3-642-31612-8_13},
)
@inproceedings(Ho&12,
 author       = {H. Hojjat and F. Konecn{\'y} and F. Garnier and R. Iosif and V. Kuncak and P. R{\"u}mmer},
 year         = {2012},
 title        = {A Verification Toolkit for Numerical Transition Systems},
 editor       = {D. Giannakopoulou and D. M{\'e}ry},
 booktitle    = {FM~'12: {F}ormal Methods, 18th International Symposium, Paris, France, August 27--31, 2012. Proceedings},
 series       = {Lecture Notes in Computer Science 7436},
 publisher    = {Springer},
 pages        = {247--251},
 doi          = {10.1007/978-3-642-32759-9_21},
)
@inproceedings(Ka&16,
 author       = {B. Kafle and J. P. Gallagher and J. F. Morales},
 year         = {2016},
 title        = {{RAHFT}: {A} Tool for Verifying {H}orn Clauses Using Abstract Interpretation and Finite Tree Automata},
 editor       = {S. Chaudhuri and A. Farzan},
 booktitle    = {Computer Aided Verification, 28th International Conference, {CAV} 2016, Toronto, ON, Canada, July 17-23, 2016, Proceedings, Part {I}},
 series       = {Lecture Notes in Computer Science 9779},
 publisher    = {Springer},
 pages        = {261--268},
 doi          = {10.1007/978-3-319-41528-4_14},
)
@techreport(Le&17,
 author       = {X. Leroy and D. Doligez and A. Frisch and J. Garrigue and D. R\'emy and J. Vouillon},
 year         = {2017},
 title        = {The {OC}aml system, {R}elease 4.06},
 type         = {Documentation and user's manual},
 institution  = {Institut {N}ational de {R}echerche en {I}nformatique et en {A}utomatique, {F}rance},
)
@inproceedings(McM03,
 author       = {K. L. McMillan},
 year         = {2003},
 title        = {Interpolation and {SAT}-Based Model Checking},
 editor       = {Warren A. Hunt Jr. and Fabio Somenzi},
 booktitle    = {Computer Aided Verification, 15th International Conference, {CAV} 2003, Boulder, CO, USA, July 8-12, 2003, Proceedings},
 series       = {Lecture Notes in Computer Science 2725},
 publisher    = {Springer},
 pages        = {1--13},
 doi          = {10.1007/978-3-540-45069-6_1},
)
@inproceedings(MoF17,
 author       = {D. Mordvinov and G. Fedyukovich},
 year         = {2017},
 title        = {Synchronizing Constrained {H}orn Clauses},
 editor       = {T. Eiter and D. Sands},
 booktitle    = {LPAR-21, 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Maun, Botswana, May 7-12, 2017},
 series       = {EPiC Series in Computing},
 volume       = {46},
 publisher    = {EasyChair},
 pages        = {338--355},
 doi          = {10.29007/gr5c},
)
@inproceedings(DeB08,
 author       = {L. M. de Moura and Bj{\o}rner, N.},
 year         = {2008},
 title        = {Z3: {A}n Efficient {SMT} Solver},
 editor       = {C.R. Ramakrishnan and J. Rehof},
 booktitle    = {Proceedings of the 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, {TACAS}~'08},
 series       = {Lecture Notes in Computer Science 4963},
 publisher    = {Springer},
 pages        = {337--340},
 doi          = {10.1007/978-3-540-78800-3_24},
)
@inproceedings(PeP00a,
 author       = {A. Pettorossi and M. Proietti},
 year         = {2000},
 title        = {Perfect Model Checking via Unfold/Fold Transformations},
 editor       = {J. W. Lloyd},
 booktitle    = {Proceedings of the First International Conference on Computational Logic (CL 2000), London, UK, 24-28 July},
 series       = {Lecture Notes in Artificial Intelligence 1861},
 publisher    = {Springer-Verlag},
 pages        = {613--628},
 doi          = {10.1007/3-540-44957-4_41},
)
@inproceedings(ReK15,
 author       = {A. Reynolds and V. Kuncak},
 year         = {2015},
 title        = {Induction for {SMT} Solvers},
 editor       = {Deepak D'Souza and Akash Lal and Kim Guldstrand Larsen},
 booktitle    = {Verification, Model Checking, and Abstract Interpretation - Proceedings of the 16th International Conference, {VMCAI} 2015, Mumbai, India,},
 series       = {Lecture Notes in Computer Science 8931},
 publisher    = {Springer},
 pages        = {80--98},
 doi          = {10.1007/978-3-662-46081-8_5},
)
@inproceedings(SaT84,
 author       = {T. Sato and H. Tamaki},
 year         = {1984},
 title        = {Transformational Logic Program Synthesis},
 booktitle    = {Proceedings of the International Conference on Fifth Generation Computer Systems},
 publisher    = {ICOT},
 pages        = {195--201},
)
@inproceedings(TaS84,
 author       = {H. Tamaki and T. Sato},
 year         = {1984},
 title        = {Unfold/Fold Trans\-form\-ation of Logic Pro\-grams},
 editor       = {S.-{\r A}. T{{\"a}}rnlund},
 booktitle    = {Proceedings of the Second International Conference on Logic Pro\-gramming,~ICLP~'84},
 publisher    = {Uppsala University},
 address      = {Uppsala, Sweden},
 pages        = {127--138},
)
@inproceedings(Un&17,
 author       = {H. Unno and S. Torii and H. Sakamoto},
 year         = {2017},
 title        = {Automating Induction for Solving {H}orn Clauses},
 editor       = {Rupak Majumdar and Viktor Kuncak},
 booktitle    = {Proc. Computer Aided Verification - 29th Intern. Conf. {CAV} 2017, Heidelberg, Germany, Part {II}},
 series       = {Lecture Notes in Computer Science 10427},
 publisher    = {Springer},
 pages        = {571--591},
 doi          = {10.1007/978-3-319-63390-9_30},
)