@inproceedings(Bj&15,
 author       = {Bj{\o}rner, N. and A. Gurfinkel and K. L. McMillan and A. Rybalchenko},
 year         = {2015},
 title        = {Horn Clause Solvers for Program Verification},
 editor       = {L. D. Beklemishev and A. Blass and N. Dershowitz and B. Finkbeiner and W. Schulte},
 booktitle    = {Fields of Logic and Computation {II} - Essays Dedicated to Yuri Gurevich on the Occasion of His 75th Birthday},
 series       = {Lecture Notes inComputer Science 9300},
 publisher    = {Springer},
 pages        = {24--51},
 doi          = {10.1007/978-3-319-23534-9\_2},
)
@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},
)
@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},
 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},
 url          = {http://www.sciencedirect.com/science/article/pii/S016764231630199X},
 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&19a,
 author       = {{De Angelis}, E. and F. Fioravanti and A. Pettorossi and M. Proietti},
 year         = {2019},
 title        = {Lemma Generation for {H}orn Clause Satisfiability: A Preliminary Study},
 editor       = {A. Lisitsa and A. Nemytykh},
 booktitle    = {Proceedings of {VPT 2019} Workshop on Program Verification and Program Transformation, Genova, Italy, April 4th, 2019},
 series       = {To appear in EPTCS},
 url          = {http://refal.botik.ru/vpt/vpt2019/VPT2019_paper_9.pdf},
)
@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(Fe&18,
 author       = {G. Fedyukovich and S. Prabhu and K. Madhukar and A. Gupta},
 year         = {2018},
 title        = {Solving Constrained Horn Clauses Using Syntax and Data},
 editor       = {Bj{\o}rner, N. and A. Gurfinkel},
 booktitle    = {2018 Formal Methods in Computer Aided Design, {FMCAD} 2018, Austin, TX, USA, October 30 - November 2, 2018},
 publisher    = {{IEEE}},
 pages        = {1--9},
 doi          = {10.23919/FMCAD.2018.8603011},
)
@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(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(HoR18,
 author       = {H. Hojjat and P. R{\"{u}}mmer},
 year         = {2018},
 title        = {The {ELDARICA} Horn Solver},
 editor       = {Bj{\o}rner, N. and A. Gurfinkel},
 booktitle    = {2018 Formal Methods in Computer Aided Design, {FMCAD} 2018, Austin, TX, USA, October 30 - November 2, 2018},
 publisher    = {{IEEE}},
 pages        = {1--7},
 doi          = {10.23919/FMCAD.2018.8603013},
)
@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},
 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},
)
@inproceedings(Ko&14,
 author       = {A. Komuravelli and A. Gurfinkel and S. Chaki},
 year         = {2014},
 title        = {SMT-Based Model Checking for Recursive Programs},
 editor       = {A. Biere and R. Bloem},
 booktitle    = {Computer Aided Verification - 26th International Conference, {CAV} 2014, Held as Part of the Vienna Summer of Logic, {VSL} 2014, Vienna, Austria, July 18-22, 2014. Proceedings},
 series       = {Lecture Notes in Computer Science 8559},
 publisher    = {Springer},
 pages        = {17--34},
 doi          = {10.1007/978-3-319-08867-9\_2},
)
@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(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},
 url          = {https://easychair.org/publications/paper/LlxW},
)
@inproceedings(DeB08,
 author       = {L. M. de Moura and Bj{\o}rner, N.},
 year         = {2008},
 title        = {Z3: {A}n Efficient {SMT} Solver},
 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(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(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},
)