@inproceedings(DBLP:conf/tacas/BallPR01,
 author       = {T. Ball and A. Podelski and S. K. Rajamani},
 year         = {2001},
 title        = {Boolean and Cartesian Abstraction for Model Checking {C} Programs},
 editor       = {T. Margaria and W. Yi},
 booktitle    = {Tools and Algorithms for the Construction and Analysis of Systems, 7th International Conference, {TACAS} 2001, Proceedings},
 series       = {Lecture Notes in Computer Science},
 volume       = {2031},
 publisher    = {Springer},
 pages        = {268--283},
 doi          = {10.1007/3-540-45319-9\_19},
)
@inproceedings(DBLP:conf/slp/BenkerimiL90,
 author       = {K. Benkerimi and J. W. Lloyd},
 year         = {1990},
 title        = {A Partial Evaluation Procedure for Logic Programs},
 editor       = {S. K. Debray and M. V. Hermenegildo},
 booktitle    = {Logic Programming, Proceedings of the 1990 North American Conference},
 publisher    = {{MIT} Press},
 pages        = {343--358},
)
@inproceedings(DBLP:conf/birthday/BjornerGMR15,
 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}},
 series       = {LNCS},
 volume       = {9300},
 publisher    = {Springer},
 pages        = {24--51},
 doi          = {10.1007/978-3-319-23534-9\_2},
)
@inproceedings(Cousot-Cousot,
 author       = {P. Cousot and R. Cousot},
 year         = {{1977}},
 title        = {Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints},
 booktitle    = {Proceedings of the 4th ACM Symposium on Principles of Programming Languages, Los Angeles},
 pages        = {238--252},
 doi          = {10.1145/512950.512973},
)
@inproceedings(Cousot-Cousot-92,
 author       = {P. Cousot and R. Cousot},
 year         = {{1992}},
 title        = {Comparing the Galois Connection and Widening/Narrowing Approaches to Abstract Interpretation},
 booktitle    = {4th International Symposium on Programming Language Implementation and Logic Programming},
 series       = {Springer-Verlag Lecture Notes in Computer Science},
 volume       = {631},
 pages        = {269--295},
 doi          = {10.1007/3-540-55844-6\_142},
)
@inproceedings(DBLP:conf/lopstr/AngelisFPP12,
 author       = {{De Angelis}, E. and F. Fioravanti and A. Pettorossi and M. Proietti},
 year         = {2012},
 title        = {Specialization with Constrained Generalization for Software Model Checking},
 editor       = {E. Albert},
 booktitle    = {{LOPSTR} 2012},
 series       = {Lecture Notes in Computer Science},
 volume       = {7844},
 publisher    = {Springer},
 pages        = {51--70},
 doi          = {10.1007/978-3-642-38197-3\_5},
)
@article(DBLP:journals/scp/AngelisFPP14,
 author       = {{De Angelis}, E. and F. Fioravanti and A. Pettorossi and M. Proietti},
 year         = {2014},
 title        = {Program verification via iterated specialization},
 journal      = {Sci. Comput. Program.},
 volume       = {95},
 pages        = {149--175},
 doi          = {10.1016/j.scico.2014.05.017},
)
@article(DeAngelisFPP18,
 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},
)
@inproceedings(DomenechGG2018,
 author       = {J. Dom\'{e}nech and S. Genaim and J. P. Gallagher},
 year         = {2018},
 title        = {Control-Flow Refinement via Partial Evaluation},
 editor       = {S. Lucas},
 booktitle    = {16th International Workshop on Termination (WST 2018)},
 pages        = {55--59},
 url          = {http://wst2018.webs.upv.es/wst2018proceedings.pdf},
)
@article(EtG96,
 author       = {S. Etalle and M. Gabbrielli},
 year         = {1996},
 title        = {Transformations of {CLP} Modules},
 journal      = {Theoretical Computer Science},
 volume       = {166},
 pages        = {101--146},
 doi          = {10.1016/0304-3975(95)00148-4},
)
@article(DBLP:journals/fuin/FioravantiPPS13,
 author       = {F. Fioravanti and A. Pettorossi and M. Proietti and V. Senni},
 year         = {2013},
 title        = {Controlling Polyvariance for Specialization-based Verification},
 journal      = {Fundam. Inform.},
 volume       = {124},
 number       = {4},
 pages        = {483--502},
 doi          = {10.3233/FI-2013-845},
)
@inproceedings(gallagher:pepm93,
 author       = {J. P. Gallagher},
 year         = {1993},
 title        = {Specialisation of Logic Programs: A Tutorial},
 booktitle    = {Proceedings PEPM'93, ACM SIGPLAN Symposium on Partial Evaluation and Semantics-Based Program Manipulation},
 publisher    = {ACM Press},
 address      = {Copenhagen},
 pages        = {88--98},
 doi          = {10.1145/154630.154640},
)
@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 Lecture Notes in Computer Science},
 volume       = {1110},
 pages        = {115--136},
 doi          = {10.1007/3-540-61580-6\_7},
)
@article(DBLP:journals/lisp/GallagherP01,
 author       = {J. P. Gallagher and J. C. Peralta},
 year         = {2001},
 title        = {Regular Tree Languages as an Abstract Domain in Program Specialisation},
 journal      = {Higher-Order and Symbolic Computation},
 volume       = {14},
 number       = {2-3},
 pages        = {143--172},
 doi          = {10.1023/A:1012936614361},
)
@inproceedings(GrebenshchikovLPR12,
 author       = {S. Grebenshchikov and N. P. Lopes and C. Popeea and A. Rybalchenko},
 year         = {2012},
 title        = {Synthesizing software verifiers from proof rules},
 editor       = {J. Vitek and H. Lin and F. Tip},
 booktitle    = {ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI '12},
 publisher    = {ACM},
 pages        = {405--416},
 doi          = {10.1145/2254064.2254112},
)
@inproceedings(DBLP:conf/pldi/GulwaniJK09,
 author       = {S. Gulwani and S. Jain and E. Koskinen},
 year         = {2009},
 title        = {Control-flow refinement and progress invariants for bound analysis},
 editor       = {M. Hind and A. Diwan},
 booktitle    = {{PLDI} 2009},
 publisher    = {{ACM}},
 pages        = {375--385},
 doi          = {10.1145/1542476.1542518},
)
@book(Jones-Gomard-Sestoft,
 author       = {N. D. Jones and C. Gomard and P. Sestoft},
 year         = {1993},
 title        = {{P}artial {E}valuation and {A}utomatic {S}oftware {G}eneration},
 publisher    = {Prentice Hall},
 doi          = {10.1016/j.scico.2004.03.010},
)
@article(DBLP:journals/tplp/KafleGGS18,
 author       = {B. Kafle and J. P. Gallagher and G. Gange and P. Schachte and S{\o}ndergaard, H. and P. J. Stuckey},
 year         = {2018},
 title        = {An iterative approach to precondition inference using constrained {H}orn clauses},
 journal      = {{TPLP}},
 volume       = {18},
 number       = {3-4},
 pages        = {553--570},
 doi          = {10.1017/S1471068418000091},
)
@article(DBLP:journals/tplp/KafleGG18,
 author       = {B. Kafle and J. P. Gallagher and P. Ganty},
 year         = {2018},
 title        = {Tree dimension in verification of constrained Horn clauses},
 journal      = {{TPLP}},
 volume       = {18},
 number       = {2},
 pages        = {224--251},
 doi          = {10.1017/S1471068418000030},
)
@inproceedings(Leuschel-Martens-96,
 author       = {M. Leuschel and B. Martens},
 year         = {1996},
 title        = {Global Control for Partial Deduction through Characteristic Atoms and Global Trees},
 editor       = {O. Danvy and R. Gl{\"u}ck and P. Thiemann},
 booktitle    = {Partial Evaluation},
 series       = {Springer-Verlag Lecture Notes in Computer Science},
 volume       = {1110},
 pages        = {263--283},
 doi          = {10.1007/3-540-61580-6\_13},
)
@inproceedings(Leuschel-Massart-LOPSTR99,
 author       = {M. Leuschel and T. Massart},
 year         = {2000},
 title        = {Infinite State Model Checking by Abstract Interpretation and Program Specialisation},
 editor       = {A. Bossi},
 booktitle    = {Logic-Based Program Synthesis and Transformation (LOPSTR'99)},
 series       = {Springer-Verlag Lecture Notes in Computer Science},
 volume       = {1817},
 pages        = {63--82},
 doi          = {10.1007/10720327\_5},
)
@article(Lloyd-Shepherdson-91,
 author       = {J. Lloyd and J. Shepherdson},
 year         = {1991},
 title        = {Partial {E}valuation in {L}ogic {P}rogramming},
 journal      = {Journal of Logic Programming},
 volume       = {11(3 \& 4)},
 pages        = {217--242},
 doi          = {10.1016/0743-1066(91)90027-M},
)
@inproceedings(Martens-Gallagher-ICLP95,
 author       = {B. Martens and J. P. Gallagher},
 year         = {1995},
 title        = {Ensuring Global Termination of Partial Deduction While Allowing Flexible Polyvariance},
 editor       = {L. Sterling},
 booktitle    = {Proc. International Conference on Logic Programming, (ICLP'95), Tokyo},
 publisher    = {MIT Press},
)
@article(Pettorossi-Proietti,
 author       = {A. Pettorossi and M. 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},
)
@article(DBLP:journals/ngc/Sahlin93,
 author       = {D. Sahlin},
 year         = {1993},
 title        = {Mixtus: An Automatic Partial Avaluator for Full Prolog},
 journal      = {New Generation Comput.},
 volume       = {12},
 number       = {1},
 pages        = {7--51},
 doi          = {10.1007/BF03038271},
)
@inproceedings(DBLP:conf/cav/SharmaDDA11,
 author       = {R. Sharma and I. Dillig and T. Dillig and A. Aiken},
 year         = {2011},
 title        = {Simplifying Loop Invariant Generation Using Splitter Predicates},
 editor       = {G. Gopalakrishnan and S. Qadeer},
 booktitle    = {Computer Aided Verification, {CAV} 2011},
 series       = {Lecture Notes in Computer Science},
 volume       = {6806},
 publisher    = {Springer},
 pages        = {703--719},
 doi          = {10.1007/978-3-642-22110-1\_57},
)
@inproceedings(Turchin-88,
 author       = {V. Turchin},
 year         = {1988},
 title        = {The Algorithm of generalization in the supercompiler},
 editor       = {Bj{\o}rner, D. and A. Ershov and N. Jones},
 booktitle    = {Proc. of the IFIP TC2 Workshop on Partial Evaluation and Mixed Computation},
 publisher    = {North-Holland},
 pages        = {531--549},
)
@inproceedings(deWaal-Gallagher-CADE12,
 author       = {D. de Waal and J. P. Gallagher},
 year         = {1994},
 title        = {The Applicability of Logic Program Analysis and Transformation to Theorem Proving},
 booktitle    = {Proceedings of the 12th International Conference on Automated Deduction (CADE-12), Nancy},
 doi          = {10.1007/3-540-58156-1\_15},
)