@incollection(Al&07,
 author       = {E. Albert and G\'{o}mez-Zamalloa, M. and L. Hubert and G. Puebla},
 year         = {2007},
 title        = {Verification of {J}ava {B}ytecode {U}sing {A}nalysis and {T}ransformation of {L}ogic {P}rograms},
 editor       = {M. Hanus},
 booktitle    = {Practical {A}spects of {D}eclarative {L}anguages},
 series       = {Lecture Notes in Computer Science 4354},
 publisher    = {Springer},
 pages        = {124--139},
 doi          = {10.1007/978-3-540-69611-7\_8},
)
@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},
)
@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: {\rm http://www.map.uniroma2.it/VeriMAP}},
)
@inproceedings(De&15b,
 author       = {{De Angelis}, E. and F. Fioravanti and A. Pettorossi and M. Proietti},
 year         = {2015},
 title        = {Semantics-based generation of verification conditions by program specialization},
 booktitle    = {Proceedings of the 17th International Symposium on Principles and Practice of Declarative Programming, Siena, Italy, July 14-16, 2015},
 publisher    = {ACM},
 pages        = {91--102},
 doi          = {10.1145/2790449.2790529},
)
@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},
)
@article(GaK14a,
 author       = {J. P. Gallagher and B. Kafle},
 year         = {2014},
 title        = {Analysis and {T}ransformation {T}ools for {C}onstrained {H}orn {C}lause {V}erification},
 journal      = {Theory and Practice of Logic Programming},
 volume       = {14},
 number       = {4-5},
 pages        = {90--101},
 note         = {Supplementary Materials},
)
@inproceedings(Gu&15,
 author       = {A. Gurfinkel and T. Kahsai and A. Komuravelli and J.A. Navas},
 year         = {2015},
 title        = {The {SeaHorn} {V}erification {F}ramework},
 booktitle    = {Computer Aided Verification: 27th International Conference, CAV 2015, San Francisco, CA, USA, July 18-24, 2015},
 publisher    = {Springer},
 pages        = {343--361},
 doi          = {10.1007/978-3-319-21690-4\_20},
)
@inproceedings(HeG06,
 author       = {K. S. Henriksen and J. P. Gallagher},
 year         = {2006},
 title        = {Abstract Interpretation of PIC Programs through Logic Programming},
 booktitle    = {Proceedings of the 6th IEEE International Workshop on Source Code Analysis and Manipulation, SCAM~'06},
 pages        = {103--179},
 doi          = {10.1109/SCAM.2006.1},
)
@inproceedings(LeS96,
 author       = {M. Leuschel and S{\o}rensen, M. H.},
 year         = {1996},
 title        = {Redundant Argument Filtering of Logic Programs},
 editor       = {J. Gallagher},
 booktitle    = {Logic Pro\-gram Synthesis and Trans\-form\-ation, Proceedings LOPSTR '96, Stockholm, Sweden},
 series       = {Lecture Notes in Computer Science 1207},
 publisher    = {Springer-Verlag},
 pages        = {83--103},
 doi          = {10.1007/3-540-62718-9\_6},
)
@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(Pe&98,
 author       = {J. C. Peralta and J. P. Gallagher and H. Saglam},
 year         = {1998},
 title        = {Analysis of {I}mperative {P}rograms through {A}nalysis of {C}onstraint {L}ogic {P}rograms},
 editor       = {G. {L}evi},
 booktitle    = {Proceedings of the 5th {I}nternational {S}ymposium on {S}tatic {A}nalysis, {SAS}~'98},
 series       = {Lecture Notes in Computer Science 1503},
 publisher    = {Springer},
 pages        = {246--261},
 doi          = {10.1007/3-540-49727-7\_15},
)
@article(PrP95a,
 author       = {M. Proietti and A. Pettorossi},
 year         = {1995},
 title        = {Unfolding-Definition-Folding, in this Order, for Avoiding Unnecessary Variables in Logic Pro\-grams},
 journal      = {Theoretical Computer Science},
 volume       = {142},
 number       = {1},
 pages        = {89--124},
 doi          = {10.1016/0304-3975(94)00227-A},
)