@article(Abdulla,
 author       = {Parosh Aziz Abdulla and Mohamed Faouzi Atig and Yu-Fang Chen and Bui Phi Diep and Hol\'{\i}k, Luk\'{a}\v{s} and Ahmed Rezine and Philipp R\"{u}mmer},
 year         = {2017},
 title        = {Flatten and Conquer: {A} Framework for Efficient Analysis of String Constraints},
 journal      = {SIGPLAN Not.},
 volume       = {52},
 number       = {6},
 pages        = {602--617},
 doi          = {10.1145/3140587.3062384},
)
@article(Leuschel2008,
 author       = {S. Barker and M. Leuschel and M. Varea},
 year         = {2008},
 title        = {Efficient and Flexible Access Control via {J}ones-optimal Logic Program Specialisation},
 journal      = {High. Order Symb. Comput.},
 volume       = {21},
 number       = {1--2},
 pages        = {5--35},
 doi          = {10.1007/s10990-008-9030-8},
)
@article(BenAbram,
 author       = {Ben-Amram, A. and N. Jones},
 year         = {2000},
 title        = {Computational Complexity via Programming Languages: Constant Factors Do Matter},
 journal      = {Acta Informatica},
 volume       = {2},
 number       = {37},
 pages        = {83--120},
 doi          = {10.1007/s002360000038},
)
@inproceedings(Bjorner,
 author       = {Bj{\o}rner, Nikolaj and Nikolai Tillmann and Andrei Voronkov},
 year         = {2009},
 title        = {Path Feasibility Analysis for String-Manipulating Programs},
 editor       = {Stefan Kowalewski and Anna Philippou},
 booktitle    = {Tools and Algorithms for the Construction and Analysis of Systems},
 publisher    = {Springer Berlin Heidelberg},
 address      = {Berlin, Heidelberg},
 pages        = {307--321},
 doi          = {10.1007/978-3-642-00768-2\_27},
)
@article(Burst,
 author       = {R. M. Burstall and John Darlington},
 year         = {1977},
 title        = {A Transformation System for Developing Recursive Programs},
 journal      = {J. ACM},
 volume       = {24},
 number       = {1},
 pages        = {44--67},
 doi          = {10.1145/321992.321996},
)
@article(Ostrich,
 author       = {Taolue Chen and Matthew Hague and Anthony W. Lin and Philipp R\"{u}mmer and Zhilin Wu},
 year         = {2019},
 title        = {Decision Procedures for Path Feasibility of String-Manipulating Programs with Complex Operations},
 journal      = {POPL},
 volume       = {3},
 pages        = {1--30},
 doi          = {10.1145/3290362},
)
@article(KarhumCombWo,
 author       = {Christian Choffrut and Juhani Karhum\"{a}ki},
 year         = {1997},
 title        = {Combinatorics of Words},
 journal      = {Handbook of Formal Languages},
 pages        = {329--438},
 doi          = {10.1007/978-3-642-59136-5\_6},
)
@inproceedings(Day2019Woorjpe,
 author       = {J. D. Day and Thorsten Ehlers and Mitja Kulczynski and Florin Manea and Dirk Nowotka and Danny Bogsted Poulsen},
 year         = {2019},
 title        = {On Solving Word Equations Using {S}{A}{T}},
 booktitle    = {Reachability Problems. RP 2019},
 volume       = {11674},
 publisher    = {Lecture Notes in Computer Science},
 pages        = {93--106},
 doi          = {10.1007/978-3-030-30806-3\_8},
)
@inproceedings(Day2017RegOrd,
 author       = {Joel D. Day and Florin Manea and Dirk Nowotka},
 year         = {2017},
 title        = {The Hardness of Solving Simple Word Equations},
 booktitle    = {42nd International Symposium on Mathematical Foundations of Computer Science (MFCS 2017)},
 series       = {Leibniz International Proceedings in Informatics (LIPIcs)},
 volume       = {83},
 pages        = {18:1--18:14},
 doi          = {10.4230/LIPIcs.MFCS.2017.18},
)
@article(Pettorossi2019,
 author       = {{De Angelis}, Emanuele and Fabio Fioravanti and Alberto Pettorossi and Maurizio Proietti},
 year         = {2018},
 title        = {Solving {H}orn Clauses on Inductive Data Types Without Induction},
 journal      = {Theory Pract. Log. Program.},
 volume       = {18},
 number       = {3--4},
 pages        = {452--469},
 doi          = {10.1017/S1471068418000157},
)
@article(Gallagher2019,
 author       = {Jes{\'{u}}s J. Dom{\'{e}}nech and John P. Gallagher and Samir Genaim},
 year         = {2019},
 title        = {Control-Flow Refinement by Partial Evaluation, and its Application to Termination and Cost Analysis},
 journal      = {Theory Pract. Log. Program.},
 volume       = {19},
 number       = {5--6},
 pages        = {990--1005},
 doi          = {10.1017/S1471068419000310},
)
@article(Futamura,
 author       = {Yoshihiko Futamura},
 year         = {1999},
 title        = {Partial Evaluation of Computation Process --- An Approach to a Compiler-Compiler},
 journal      = {Higher-Order and Symbolic Computation},
 volume       = {12},
 pages        = {381--391},
 doi          = {10.1023/A:1010095604496},
)
@inproceedings(Hamilton15,
 author       = {Geoff W. Hamilton},
 year         = {2015},
 title        = {Verifying Temporal Properties of Reactive Systems by Transformation},
 booktitle    = {Proceedings of the Third International Workshop on Verification and Program Transformation, VPT@ETAPS 2015, London, United Kingdom, 11th April 2015.},
 pages        = {33--49},
 doi          = {10.4204/EPTCS.199.3},
)
@article(Hmelevsky,
 author       = {Ju. I. Hmelevskij},
 year         = {1971},
 title        = {Equations in a Free Semigroup. (in {R}ussian)},
 journal      = {Trudy Mat. Inst. Steklov},
 volume       = {107},
 pages        = {286},
)
@article(Jez,
 author       = {Artur Jez},
 year         = {2016},
 title        = {Recompression: {A} Simple and Powerful Technique for Word Equations},
 journal      = {J. ACM},
 volume       = {63},
 number       = {1},
 doi          = {10.1145/2743014},
)
@book(JonesBook2,
 author       = {Neil Jones},
 year         = {2002},
 title        = {Computability and Complexity from a Programming Perspective},
 volume       = {62},
 publisher    = {NATO Science Series, Springer},
 doi          = {10.1007/978-94-010-0413-8\_4},
)
@book(JonesBook,
 author       = {Neil Jones and Carsten Gomard and Peter Sestoft},
 year         = {1993},
 title        = {Partial Evaluation and Automatic Program Generation},
 publisher    = {Prentice Hall International},
)
@book(DiekertJewels,
 author       = {Juhani Karhum\"{a}ki and Hermann Maurer and Gheorghe Paun and Grzegorz Rozenberg},
 year         = {1999},
 title        = {Jewels are Forever, {C}ontributions on Th. Computer Science in Honor of {A}rto {S}alomaa},
 publisher    = {Springer, Berlin, Heidelberg},
 doi          = {10.1007/978-3-642-60207-8\_28},
)
@inbook(Le2018,
 author       = {Quang Loc Le and Mengda He},
 year         = {2018},
 title        = {A Decision Procedure for String Logic with Quadratic Equations, Regular Expressions and Length Constraints},
 pages        = {350--372},
 volume       = {11275},
 publisher    = {Lecture Notes in Computer Science},
 doi          = {10.1007/978-3-030-02768-1\_19},
)
@article(CVC4,
 author       = {Tianyi Liang and Andrew Reynolds and Nestan Tsiskaridze and Cesare Tinelli and Clark Barrett and Morgan Deters},
 year         = {2016},
 title        = {An Efficient {S}{M}{T} Solver for String Constraints},
 journal      = {Form. Methods Syst. Des.},
 volume       = {48},
 number       = {3},
 pages        = {206--234},
 doi          = {10.1007/s10703-016-0247-6},
)
@inproceedings(Lin2018,
 author       = {Anthony Widjaja Lin and Rupak Majumdar},
 year         = {2018},
 title        = {Quadratic Word Equations with Length Constraints, Counter Systems, and {P}resburger Arithmetic with Divisibility},
 booktitle    = {Automated Technology for Verification and Analysis. ATVA 2018},
 volume       = {11138},
 publisher    = {Lecture Notes in Computer Science},
 pages        = {352--369},
 doi          = {10.1007/978-3-030-01090-4\_21},
)
@inproceedings(NemytykhCSR,
 author       = {Alexei Lisitsa and Andrei P. Nemytykh},
 year         = {2007},
 title        = {A Note on Specialization of Interpreters},
 editor       = {Volker Diekert and Mikhail V. Volkov and Andrei Voronkov},
 booktitle    = {Computer Science -- Theory and Applications},
 publisher    = {Springer Berlin Heidelberg},
 pages        = {237--248},
 doi          = {10.1007/978-3-540-74510-5\_25},
)
@article(NemReachability,
 author       = {Alexei Lisitsa and Andrei P. Nemytykh},
 year         = {2008},
 title        = {Reachability Analysis in Verification via Supercompilation},
 journal      = {Int. J. Foundations of Computer Science},
 volume       = {19},
 number       = {4},
 pages        = {953--970},
 doi          = {10.1142/S0129054108006066},
)
@inproceedings(Z3,
 author       = {M. Berzish, V. Ganesh and Y. Zheng},
 year         = {2017},
 title        = {Z3str3: {A} String Solver with Theory-aware Heuristics},
 booktitle    = {Formal Methods in Computer Aided Design (FMCAD)},
 pages        = {55--59},
 doi          = {10.23919/FMCAD.2017.8102241},
)
@article(Makanin77,
 author       = {Gennadiy S. Makanin},
 year         = {1977},
 title        = {The Problem of Solvability of Equations in a~Free Semigroup},
 journal      = {Math. USSR-Sb.},
 volume       = {32},
 number       = {2},
 pages        = {129--198},
 doi          = {10.1070/SM1977v032n02ABEH002376},
)
@article(Matiyas,
 author       = {Yuri Matiyasevich},
 year         = {1968},
 title        = {A Connection between Systems of Word and Length Equations and {H}ilbert's {T}enth {P}roblem (in {R}ussian)},
 journal      = {Sem. Mat. V. A. Steklov Math. Inst. Leningrad},
 volume       = {8},
 pages        = {132--144},
)
@book(NemytykhBook,
 author       = {A. P. Nemytykh},
 year         = {2007},
 title        = {The Supercompiler {S}{C}{P}4: General Structure (in {R}ussian)},
 publisher    = {URSS, Moscow},
)
@inproceedings(NemytykhUnfold,
 author       = {Andrei P. Nemytykh},
 year         = {2014},
 title        = {On Unfolding for Programs Using Strings as a Data Type},
 booktitle    = {{VPT} 2014. Second International Workshop on Verification and Program Transformation, July 17--18, 2014, Vienna, Austria, co-located with the 26th International Conference on Computer Aided Verification {CAV 2014}},
 pages        = {66--83},
 doi          = {10.29007/m8rr},
)
@article(NepeivodaArt,
 author       = {Antonina Nepeivoda},
 year         = {2016},
 title        = {Ping-pong Protocols as Prefix Grammars: {M}odelling and Verification via Program Transformation},
 journal      = {Journal of Logical and Algebraic Methods in Programming},
 volume       = {85},
 number       = {5},
 pages        = {782--804},
 doi          = {10.1016/j.jlamp.2016.06.001},
 note         = {Special Issue on Automated Verification of Programs and Web Systems},
)
@inproceedings(Pettorossi96,
 author       = {Alberto Pettorossi and Maurizio Proietti},
 year         = {1996},
 title        = {A Comparative Revisitation of Some Program Transformation Techniques},
 booktitle    = {Partial Evaluation},
 publisher    = {Springer Berlin Heidelberg},
 address      = {Berlin, Heidelberg},
 pages        = {355--385},
 doi          = {10.1007/3-540-61580-6\_18},
)
@inproceedings(Plandowski,
 author       = {Wojciech Plandowski},
 year         = {2006},
 title        = {An Efficient Algorithm for Solving Word Equations},
 booktitle    = {Proceedings of 38th Annual ACM Symposium on Theory of Computing},
 publisher    = {Association for Computing Machinery},
 address      = {New York, NY, USA},
 pages        = {467--476},
 doi          = {10.1145/1132516.1132584},
)
@inproceedings(Saxena,
 author       = {P. Saxena and D. Akhawe and S. Hanna and F. Mao and S. McCamant and D. Song},
 year         = {2010},
 title        = {A Symbolic Execution Framework for {J}avascript},
 booktitle    = {SP},
 pages        = {513--528},
 doi          = {10.1109/SP.2010.38},
)
@inproceedings(SecherSorensen99,
 author       = {Jens P. Secher and S{\o}rensen, Morten Heine},
 year         = {1999},
 title        = {On Perfect Supercompilation},
 booktitle    = {Perspectives of System Informatics, Third International Andrei Ershov Memorial Conference, PSI'99, Akademgorodok, Novosibirsk, Russia, July 6--9, 1999, Proceedings},
 pages        = {113--127},
 doi          = {10.1007/3-540-46562-6\_10},
)
@inproceedings(Sorensen95,
 author       = {S{\o}rensen, Morten H. and Robert Gl\"{u}ck},
 year         = {1995},
 title        = {An Algorithm of Generalization in Positive Supercompilation},
 booktitle    = {Proceedings of ILPS'95, the International Logic Programming Symposium},
 publisher    = {MIT Press},
 pages        = {465--479},
 doi          = {10.7551/mitpress/4301.003.0048},
)
@article(Jones,
 author       = {S\o{}rensen, Morten H. and Robert Gl\"uck and Neil D. Jones},
 year         = {1993},
 title        = {A Positive Supercompiler},
 journal      = {Journal of Functional Programming},
 volume       = {6},
 pages        = {465--479},
 doi          = {10.1017/s0956796800002008},
)
@inproceedings(Trinh,
 author       = {M.-T. Trinh and D.-H. Chu and D.-H. Jaffar},
 year         = {2016},
 title        = {Progressive Reasoning over Recursively-Defined Strings},
 booktitle    = {Proc. CAV 2016 (LNCS)},
 volume       = {9779},
 pages        = {218--240},
 doi          = {10.1007/978-3-319-41528-4\_12},
)
@article(Tur86,
 author       = {Valentin 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},
)
@book(TurRefal5,
 author       = {Valentin 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/}},
)
@inproceedings(TurGener,
 author       = {Valentin F. Turchin},
 year         = {1996},
 title        = {On Generalization of Lists and Strings in Supercompilation},
 booktitle    = {Technical Report CSc. TR 96-002},
 publisher    = {City College of the City University of New York},
 pages        = {1--28},
)
@article(Vidal12,
 author       = {Germ{\'{a}}n Vidal},
 year         = {2012},
 title        = {Annotation of Logic Programs for Independent {A}{N}{D}-parallelism by Partial Evaluation},
 journal      = {Theory Pract. Log. Program.},
 volume       = {12},
 number       = {4--5},
 pages        = {583--600},
 doi          = {10.1017/S1471068412000191},
)
@inproceedings(Yu,
 author       = {Fang Yu and Tevfik Bultan and Oscar H. Ibarra},
 year         = {2011},
 title        = {Relational String Verification Using Multi-track Automata},
 editor       = {Michael Domaratzki and Kai Salomaa},
 booktitle    = {Implementation and Application of Automata},
 publisher    = {Springer Berlin Heidelberg},
 address      = {Berlin, Heidelberg},
 pages        = {290--299},
 doi          = {10.1007/978-3-642-18098-9\_31},
)