@inproceedings(AhmedLisitsaNemytykh:NSPK,
 author       = {A. Ahmed and A.P. Lisitsa and A.P. Nemytykh},
 year         = {2013},
 title        = {Cryptographic Protocol Verification via Supercompilation ({A} Case Study)},
 booktitle    = {VPT 2013},
 series       = {EPiC Series},
 volume       = {16},
 publisher    = {EasyChair},
 pages        = {16--29},
 note         = {Available at URL \url{http://www.easychair.org/publications/paper/147590}},
)
@misc(Begin:BABYLON,
 author       = {L. van Begin},
 title        = {The {BABYLON} Project: A Tool for Specification and Verification of Parameterized Systems to Benchmark Infinite-State Model Checkers},
 howpublished = {[online]},
 note         = {\url{http://www.ulb.ac.be/di/ssd/lvbegin/CST/}},
)
@article(FioPettProSen:Ver-IterSpec14,
 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 / {Selected} and extended papers from Partial Evaluation and Program Manipulation 2013},
 number       = {Part 2},
 pages        = {149–--175},
 doi          = {10.1016/j.scico.2014.05.017},
)
@inproceedings(VeriMAP:2014,
 author       = {{De Angelis}, E. and F. Fioravanti and A. Pettorossi and M. Proietti},
 year         = {2014},
 title        = {{Veri{MAP}}: A Tool for Verifying Programs through Transformations},
 booktitle    = {Proc. of ({TACAS} 2014)},
 series       = {LNCS},
 volume       = {8413},
 publisher    = {Springer},
 pages        = {568–--574},
 doi          = {10.1007/978-3-642-54862-8\_47},
)
@article(FioPettProSen:Ver-Linear-Fib15,
 author       = {{De Angelis}, E. and F. Fioravanti and A. Pettorossi and M. Proietti},
 year         = {2015},
 title        = {Proving correctness of imperative programs by linearizing constrained {Horn} clauses},
 journal      = {Theory and Practice of Logic Programming},
 volume       = {15 / 31st {International} Conference on Logic Programming},
 number       = {4--5},
 pages        = {635–--650},
 doi          = {10.1017/S1471068415000289},
)
@misc(Delzanno:Automatic,
 author       = {G. Delzanno},
 title        = {Automatic Verification of Cache Coherence Protocols via Infinite-state Constraint-based Model Checking},
 howpublished = {[online]},
 note         = {\url{http://www.disi.unige.it/person/DelzannoG/protocol.html}},
)
@inproceedings(Delzanno-Param:00,
 author       = {G. Delzanno},
 year         = {2000},
 title        = {Automatic Verification of Parameterized Cache Coherence Protocols},
 booktitle    = {The {Proc.} of the 12th {Int.} {Conference} on {Computer} Aided Verification},
 series       = {LNCS},
 volume       = {1855},
 pages        = {53--68},
 doi          = {10.1007/10722167\_8},
)
@inproceedings(Delzanno-Futurebus:00,
 author       = {G. Delzanno},
 year         = {2000},
 title        = {Verification of Consistency Protocols via Infinite-state Symbolic Model Checking, {A} Case Study: the {IEEE} {Futurebus+} Protocol},
 booktitle    = {The {Proc.} of {FORTE/PSTV}},
 publisher    = {Springer US},
 pages        = {171--186},
 doi          = {10.1007/978-0-387-35533-7\_11},
)
@inproceedings(Emerson2003,
 author       = {E. A. Emerson and V. Kahlon},
 year         = {2003},
 title        = {Exact and Efficient Verification of Parameterized Cache Coherence Protocols},
 booktitle    = {the Proc. of {CHARME 2003}: 12th {IFIP} {WG} 10.5 {Advanced Research Working Conference}},
 publisher    = {Springer},
 pages        = {247--262},
 doi          = {10.1007/978-3-540-39724-3\_22},
)
@inproceedings(Esparza:1999,
 author       = {J. Esparza and A. Finkel and R. Mayr},
 year         = {1999},
 title        = {{On} the verification of broadcast protocols},
 booktitle    = {the Proc. of 14th {Symposium} Logic in {Computer} {Science}},
 organization = {IEEE},
 pages        = {352--359},
 doi          = {10.1109/LICS.1999.782630},
)
@inproceedings(FioPettPro:01,
 author       = {F. Fioravanti and A. Pettorossi and M. Proietti},
 year         = {2001},
 title        = {Verifying {CTL} properties of infinite state systems by specializing constraint logic programs},
 booktitle    = {the Proc. of {VCL}’01},
 series       = {Tech. Rep.},
 volume       = {DSSE-TR-2001-3},
 publisher    = {University of Southampton},
 address      = {UK},
 pages        = {85–--96},
 note         = {Available at \url{http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.15.9752}},
)
@inproceedings(FioPettProSen:GenVer13,
 author       = {F. Fioravanti and A. Pettorossi and M. Proietti and V. Senni},
 year         = {2013},
 title        = {Generalization Strategies for the Verification of Infinite State Systems},
 editor       = {W. Faber and N. Leone},
 booktitle    = {Theory and Practice of Logic Programming},
 volume       = {13 / {Special} Issue 02 (25th {GULP} annual conference)},
 publisher    = {Cambridge University Press},
 pages        = {175--199},
 doi          = {10.1017/S1471068411000627},
)
@inproceedings(FisherKL05,
 author       = {M. Fisher and B. Konev and A. Lisitsa},
 year         = {2006},
 title        = {Practical Infinite-State Verification with Temporal Reasoning},
 booktitle    = {Proc. of the {VISSAS} 2005},
 publisher    = {IOS Press},
 pages        = {91--100},
)
@article(Futamura:1971,
 author       = {Y. Futamura},
 year         = {1971},
 title        = {Partial evaluation of computing process – an approach to a compiler-compiler},
 journal      = {Systems, Computers, Controls},
 volume       = {2},
 number       = {5},
 pages        = {45–--50},
 doi          = {10.1023/A:1010095604496},
)
@inproceedings(GH:1998,
 author       = {J. P. Gallagher and J. C. Peralta and H. Saglam},
 year         = {1998},
 title        = {Analysis of imperative programs through analysis of Constraint Logic Programs},
 editor       = {B. Demoen and V. Lifschitz},
 booktitle    = {SAS 1998},
 series       = {LNCS},
 volume       = {1503},
 publisher    = {Springer},
 pages        = {246–--261},
 doi          = {10.1007/3-540-49727-7\_15},
)
@article(Hamilton:VPT2015,
 author       = {G. W. Hamilton},
 year         = {2015},
 title        = {Verifying Temporal Properties of Reactive Systems by Transformation},
 journal      = {Electronic Proceedings in Theoretical Computer Science},
 volume       = {199},
 pages        = {33--–49},
 doi          = {10.4204/EPTCS.199.3},
)
@article(Hamilton:VPT2016,
 author       = {G. W. Hamilton},
 year         = {2016},
 title        = {Generating Counterexamples for Model Checking by Transformation},
 journal      = {Electronic Proceedings in Theoretical Computer Science},
 volume       = {216},
 pages        = {65–--82},
 doi          = {10.4204/EPTCS.216.4},
)
@article(Higman,
 author       = {G. Higman},
 year         = {1952},
 title        = {Ordering by divisibility in abstract algebras},
 journal      = {Proc. London Math. Soc.},
 volume       = {2},
 number       = {7},
 pages        = {326--336},
 doi          = {10.1112/plms/s3-2.1.326},
)
@book(Jones:Complex,
 author       = {N. D. Jones},
 year         = {1997},
 title        = {Computability and Complexity from a Programming Perspective},
 publisher    = {The MIT Press},
 note         = {ISBN:9780262100649, Revised version (2007) is available at \url{http://www.diku.dk/~neil/comp2book2007/book-whole.pdf}},
)
@article(Jones:IntSpecialisation,
 author       = {N. D. Jones},
 year         = {2004},
 title        = {Transformation by Interpreter Specialisation},
 journal      = {Science of Computer Programming},
 volume       = {52},
 pages        = {307--339},
 doi          = {10.1016/j.scico.2004.03.010},
)
@article(Jonsson_Nordlander,
 author       = {P. A. Jonsson and J. Nordlander},
 year         = {2009},
 title        = {Positive Supercompilation for a higher order call-by-value language},
 journal      = {ACM {SIGPLAN} {Notices}},
 volume       = {44},
 number       = {1},
 pages        = {277--288},
 doi          = {10.1145/1480881.1480916},
)
@inproceedings(Klimov:PetriNets12,
 author       = {A. V. Klimov},
 year         = {2012},
 title        = {Solving Coverability Problem for Monotonic Counter Systems by Supercompilation},
 booktitle    = {the Proc. of PSI'11},
 series       = {LNCS},
 volume       = {7162},
 pages        = {193--209},
 doi          = {10.1007/978-3-642-29709-0\_18},
)
@techreport(Klyuchnikov:HOSC,
 author       = {I. Klyuchnikov},
 year         = {2010},
 title        = {Supercompiler {HOSC} 1.5: homeomorphic embedding and generalization in a higher-order setting},
 type         = {Technical Report},
 number       = {62},
 institution  = {Keldysh Institute of Applied Mathematics},
 address      = {Moscow},
)
@article(Kruskal,
 author       = {J. B. Kruskal},
 year         = {1960},
 title        = {Well-quasi-ordering, the tree theorem, and {Vazsonyi's} conjecture},
 journal      = {Trans. Amer. Math. Society},
 volume       = {95},
 pages        = {210--225},
 doi          = {10.2307/1993287},
)
@inproceedings(Leuschel:04,
 author       = {H. Lehmann and M. Leuschel},
 year         = {2004},
 title        = {Inductive Theorem Proving by Program Specialisation: Generating Proofs for {Isabelle} Using {Ecce}},
 booktitle    = {Proceedings of {LOPSTR’03}},
 series       = {LNCS},
 volume       = {3018},
 pages        = {1--19},
 doi          = {10.1007/978-3-540-25938-1\_1},
)
@inproceedings(Leuschel:98,
 author       = {M. Leuschel},
 year         = {1998},
 title        = {On the Power of Homeomorphic Embedding for Online Termination},
 booktitle    = {Proc. of the {SAS'98}},
 series       = {LNCS},
 volume       = {1503},
 pages        = {230--245},
 doi          = {10.1007/3-540-49727-7\_14},
)
@inproceedings(Lisitsa:ATVA10,
 author       = {A. Lisitsa},
 year         = {2010},
 title        = {Reachability as Derivability, Finite Countermodels and Verification},
 booktitle    = {ATVA 2010},
 series       = {LNCS},
 volume       = {6252},
 pages        = {233--244},
 doi          = {10.1007/978-3-642-15643-4\_18},
)
@article(Lis_Nem:IJFCS08,
 author       = {A. Lisitsa and A. P. Nemytykh},
 year         = {2008},
 title        = {Reachability Analysis in Verification via Supercompilation},
 journal      = {International Journal of Foundations of Computer Science},
 volume       = {19},
 number       = {4},
 pages        = {953--970},
 doi          = {10.1142/S0129054108006066},
)
@inproceedings(Lis_Nem:CSR07,
 author       = {A. P. Lisitsa and A. P. Nemytykh},
 year         = {2007},
 title        = {A Note on Specialization of Interpreters},
 booktitle    = {The 2-nd International Symposium on Computer Science in Russia (CSR-2007)},
 series       = {LNCS},
 volume       = {4649},
 pages        = {237--248},
 doi          = {10.1007/978-3-540-74510-5\_25},
)
@article(Lis_Nem:Programming,
 author       = {A. P. Lisitsa and A. P. Nemytykh},
 year         = {2007},
 title        = {Verification as Parameterized Testing ({Experiments} with the {SCP4} Supercompiler)},
 journal      = {Programmirovanie, (In {Russian})},
 volume       = {1},
 pages        = {22--34},
 doi          = {10.1134/S0361768807010033},
 note         = {English translation in \emph{J. Programming and Computer Software}, Vol. {\bfseries33}, No.1, pp: 14--23, 2007,},
)
@misc(Lis_Nem:Protocols07,
 author       = {A. P. Lisitsa and A. P. Nemytykh},
 year         = {2007--2009},
 title        = {Experiments on Verification via Supercompilation},
 howpublished = {[online]},
 note         = {\url{http://refal.botik.ru/protocols/}},
)
@inproceedings(Lis_Nem:TAP08,
 author       = {A. P. Lisitsa and A. P. Nemytykh},
 year         = {2008},
 title        = {Extracting Bugs from the Failed Proofs in Verification via Supercompilation},
 editor       = {Bernhard Beckert and Reiner Hahnle},
 booktitle    = {Tests and Proofs: Papers Presented at the Second International Conference TAP 2008},
 series       = {Reports of the Faculty of Informatics, Univesitat Koblenz-Landau},
 volume       = {5/2008},
 pages        = {49--65},
 note         = {Available at \url{http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.160.7790\&rep=rep1\&type=pdf\#page=57}},
)
@inproceedings(Lis_Nem:MissCannVPT2014,
 author       = {A. P. Lisitsa and A. P. Nemytykh},
 year         = {2014},
 title        = {A Note on Program Specialization. What Can Syntactical Properties of Residual Programs Reveal?},
 booktitle    = {VPT 2014},
 series       = {EPiC Series},
 volume       = {28},
 publisher    = {EasyChair},
 pages        = {52--65},
 note         = {Available at URL \url{http://www.easychair.org/publications/paper/183895}},
)
@misc(Lis_Nem:Veri-via-Inters-arXiv,
 author       = {A. P. Lisitsa and A. P. Nemytykh},
 year         = {2017},
 title        = {Verifying Programs via Intermediate Interpretation ({Extended} version)},
 note         = {\href{https://arxiv.org/abs/1705.06738}{arXiv:1705.06738}},
)
@inproceedings(N:03,
 author       = {A. P. Nemytykh},
 year         = {2003},
 title        = {The Supercompiler {SCP4}: {General Structure}. ({Extended} abstract)},
 booktitle    = {the Proc. of PSI'03},
 series       = {LNCS},
 volume       = {2890},
 pages        = {162--170},
 doi          = {10.1007/978-3-540-39866-0\_18},
)
@book(Nemytykh:SCP4book,
 author       = {A. P. Nemytykh},
 year         = {2007},
 title        = {The Supercompiler {SCP4}: General Structure},
 publisher    = {URSS},
 address      = {Moscow},
 note         = {(Book in {Russian}: \url{http://urss.ru/cgi-bin/db.pl?cp=&page=Book&id=55806&lang=Ru&blang=ru&list=})},
)
@inproceedings(Nem_Pin_Tur,
 author       = {A. P. Nemytykh and V. A. Pinchuk and V. F. Turchin},
 year         = {1996},
 title        = {A Self-Applicable Supercompiler},
 booktitle    = {PEPM'96},
 series       = {LNCS},
 volume       = {1110},
 publisher    = {Springer-Verlag},
 pages        = {322--337},
 doi          = {10.1007/3-540-61580-6\_16},
)
@misc(NT:00,
 author       = {A. P. Nemytykh and V. F. Turchin},
 year         = {2000},
 title        = {The Supercompiler {SCP4}: Sources, On-line Demonstration},
 howpublished = {[online]},
 note         = {\url{http://www.botik.ru/pub/local/scp/refal5/}},
)
@inproceedings(ANepeivoda:PingPong,
 author       = {Antonina Nepeivoda},
 year         = {2013},
 title        = {Ping-Pong Protocols as Prefix Grammars and {Turchin} Relation},
 booktitle    = {VPT 2013},
 series       = {EPiC Series},
 volume       = {16},
 publisher    = {EasyChair},
 pages        = {74--87},
 note         = {Available at URL \url{http://www.easychair.org/publications/paper/147593}},
)
@article(AntoninaNepeivoda:Sbornik2014,
 author       = {Antonina Nepeivoda},
 year         = {2014},
 title        = {Turchin's Relation and Loop Approximation in Program Analysis},
 journal      = {Proceedings on the Functional Language Refal (in Russian)},
 volume       = {1},
 pages        = {170--192},
 note         = {ISBN:978-5-9905410-1-6, available at {\href{http://refal.botik.ru/library/refal2014_issue-I.pdf}{http://refal.botik.ru/library/refal2014\_issue-I.pdf}}},
)
@article(AntoninaNepeivoda:VPT2016,
 author       = {Antonina Nepeivoda},
 year         = {2016},
 title        = {Turchin's Relation for Call-by-Name Computations: {A} Formal Approach},
 journal      = {Electronic Proceedings in Theoretical Computer Science},
 volume       = {216},
 pages        = {137--159},
 doi          = {10.4204/EPTCS.216.8},
)
@article(Pong:1997,
 author       = {F. Pong and M. Dubois},
 year         = {1997},
 title        = {Verification Techniques for Cache Coherence Protocols},
 journal      = {ACM Comput. Surv.},
 volume       = {29},
 number       = {1},
 pages        = {82--126},
 doi          = {10.1145/248621.248624},
)
@article(Roychoudhury:2004,
 author       = {A. Roychoudhury and I. V. Ramakrishnan},
 year         = {2004},
 title        = {Inductively verifying invariant properties of parameterized systems},
 journal      = {Automated Software Engineering},
 volume       = {11},
 number       = {2},
 pages        = {101--139},
 doi          = {10.1023/B:AUSE.0000017740.35552.88},
)
@article(SGJ:96,
 author       = {S{\o}rensen, M. H. and R. Gl\"{u}ck and N. D. Jones},
 year         = {1996},
 title        = {A Positive Supercompiler},
 journal      = {Journal of Functional Programming},
 volume       = {6},
 number       = {6},
 pages        = {811--838},
 doi          = {10.1017/S0956796800002008},
)
@techreport(Turchin:Report20,
 author       = {V. F. Turchin},
 year         = {1980},
 title        = {The language {Refal} \--- The Theory of Compilation and Metasystem Analysis},
 type         = {Technical Report},
 number       = {20},
 institution  = {Courant Institute of Mathematical Sciences, New York University},
 note         = {Available at \url{https://pdfs.semanticscholar.org/75cb/a161e01f2920c8d4668fa5c979adc7422461.pdf}},
)
@article(Tur:86,
 author       = {V. F. Turchin},
 year         = {1986},
 title        = {The Concept of a Supercompiler},
 journal      = {ACM Transactions on Programming Languages and Systems},
 volume       = {8},
 number       = {3},
 pages        = {292--325},
 doi          = {10.1145/5956.5957},
)
@inproceedings(Turchin:Generalization88,
 author       = {V. F. Turchin},
 year         = {1988},
 title        = {The Algorithm of Generalization in the Supercompiler},
 booktitle    = {Proc. of the IFIP TC2 Workshop, Partial Evaluation and Mixed Computation},
 publisher    = {North-Holland Publishing Co.},
 pages        = {531--549},
)
@book(Turchin:Refal5,
 author       = {V. F. Turchin},
 year         = {1989},
 title        = {Refal-5, Programming Guide and Reference Manual},
 publisher    = {New England Publishing Co.},
 address      = {Holyoke, Massachusetts},
 note         = {Electronic version: \url{http://www.botik.ru/pub/local/scp/refal5/}, 2000},
)
@misc(Refal5:PZ,
 author       = {V. F. Turchin and D. V. Turchin and A. P. Konyshev and A. P. Nemytykh},
 year         = {2000},
 title        = {Refal-5: Sources, Executable Modules},
 howpublished = {[online]},
 note         = {\url{http://www.botik.ru/pub/local/scp/refal5/}},
)