@inproceedings(AbrGlu:00:nsint,
 author       = {Sergei M. Abramov and Robert Gl{\"u}ck},
 year         = {2000},
 title        = {Combining semantics with non-standard interpreter hierarchies},
 editor       = {Sanjiv Kapoor and Sanjiva Prasad},
 booktitle    = {Foundations of Software Technology and Theoretical Computer Science. Proceedings},
 series       = {LNCS 1974},
 publisher    = {Springer-Verlag},
 pages        = {201--213},
 doi          = {10.1007/3-540-44450-5\_16},
)
@inproceedings(AhmedLisitsaNemytykh:13,
 author       = {Abdulbasit Ahmed and Alexei P. Lisitsa and Andrei P. Nemytykh},
 year         = {2013},
 title        = {Cryptographic protocol verification via supercompilation (a case study)},
 editor       = {Alexei P. Lisitsa and Andrei P. Nemytykh},
 booktitle    = {Verification and Program Transformation. Proceedings},
 series       = {EPiC Series in Computing},
 volume       = {16},
 pages        = {16--29},
 doi          = {10.29007/gpsh},
)
@article(AHU:68,
 author       = {Alfred V. Aho and John E. Hopcroft and Jeffrey D. Ullman},
 year         = {1968},
 title        = {Time and tape complexity of pushdown automaton languages},
 journal      = {Information and Control},
 volume       = {13},
 number       = {3},
 pages        = {186--206},
 doi          = {10.1016/S0019-9958(68)91087-5},
)
@incollection(ABE:16:handbook,
 author       = {Rajeev Alur and Ahmed Bouajjani and Javier Esparza},
 year         = {2018},
 title        = {Model checking procedural programs},
 editor       = {Edmund M. Clarke and Thomas A. Henzinger and Helmut Veith and Roderick Bloem},
 booktitle    = {Handbook of Model Checking},
 publisher    = {Springer-Verlag},
 note         = {To appear},
)
@inproceedings(AxGl11FoSSaCS,
 author       = {Holger B. Axelsen and Robert Gl{\"u}ck},
 year         = {2011},
 title        = {What do reversible programs compute?},
 editor       = {Martin Hofmann},
 booktitle    = {Foundations of Software Science and Computation Structures. Proceedings},
 series       = {LNCS 6604},
 publisher    = {Springer-Verlag},
 pages        = {42--56},
 doi          = {10.1007/978-3-642-19805-2\_4},
)
@inproceedings(Cook:72,
 author       = {Stephen A. Cook},
 year         = {1972},
 title        = {Linear time simulation of deterministic two-way pushdown automata},
 editor       = {Charles V. Freiman and John E. Griffith and Jack L. Rosenfeld},
 booktitle    = {Information Processing 71},
 publisher    = {North-Holland},
 pages        = {75--80},
)
@article(DolevEvenKarp:82,
 author       = {Danny Dolev and Shimon Even and Richard M. Karp},
 year         = {1982},
 title        = {On the security of ping-pong protocols},
 journal      = {Information and Control},
 volume       = {55},
 number       = {1-3},
 pages        = {57--68},
 doi          = {10.1016/S0019-9958(82)90401-6},
)
@inproceedings(DolevYao:81,
 author       = {Danny Dolev and Andrew C. Yao},
 year         = {1981},
 title        = {On the security of public key protocols (extended abstract)},
 booktitle    = {Foundations of Computer Science. Proceedings},
 publisher    = {IEEE Computer Society},
 pages        = {350--357},
 doi          = {10.1109/SFCS.1981.32},
)
@article(DolevYao:83,
 author       = {Danny Dolev and Andrew C. Yao},
 year         = {1983},
 title        = {On the security of public key protocols},
 journal      = {IEEE Transactions on Information Theory},
 volume       = {29},
 number       = {2},
 pages        = {198--207},
 doi          = {10.1109/TIT.1983.1056650},
)
@inproceedings(FioravantiPettorossiProietti:02,
 author       = {Fabio Fioravanti and Alberto Pettorossi and Maurizio Proietti},
 year         = {2002},
 title        = {Verification of sets of infinite state processes using program transformation},
 editor       = {Alberto Pettorossi},
 booktitle    = {Logic Based Program Synthesis and Transformation. Proceedings},
 series       = {LNCS 2372},
 publisher    = {Springer-Verlag},
 pages        = {111--128},
 doi          = {10.1007/3-540-45607-4\_7},
)
@article(Floyd:67,
 author       = {Robert W. Floyd},
 year         = {1967},
 title        = {Nondeterministic algorithms},
 journal      = {Journal of the ACM},
 volume       = {14},
 number       = {4},
 pages        = {636--644},
 doi          = {10.1145/321420.321422},
)
@article(FKG:01:NGC,
 author       = {Yoshihiko Futamura and Zenjiro Konishi and Robert Gl\"uck},
 year         = {2002},
 title        = {Program transformation system based on generalized partial computation},
 journal      = {New Generation Computing},
 volume       = {20},
 number       = {1},
 pages        = {75--99},
 doi          = {10.1007/BF03037260},
)
@article(Glueck:94:JFP,
 author       = {Robert Gl{\"u}ck},
 year         = {1994},
 title        = {On the generation of specializers},
 journal      = {Journal of Functional Programming},
 volume       = {4},
 number       = {4},
 pages        = {499--514},
 doi          = {10.1017/S0956796800001167},
)
@inproceedings(Glueck:16:pdasim,
 author       = {Robert Gl\"{u}ck},
 year         = {2016},
 title        = {A practical simulation result for two-way pushdown automata},
 editor       = {Yo-Sub Han and Kai Salomaa},
 booktitle    = {Implementation and Application of Automata. Proceedings},
 series       = {LNCS 9705},
 publisher    = {Springer-Verlag},
 pages        = {113--124},
 doi          = {10.1007/978-3-319-40946-7\_10},
)
@inproceedings(GlueckJoergensen:94:SAS,
 author       = {Robert Gl{\"u}ck and J{\o}rgensen, Jesper},
 year         = {1994},
 title        = {Generating transformers for deforestation and supercompilation},
 editor       = {Le Charlier, Baudouin},
 booktitle    = {Static Analysis. Proceedings},
 series       = {LNCS 864},
 publisher    = {Springer-Verlag},
 pages        = {432--448},
 doi          = {10.1007/3-540-58485-4\_57},
)
@inproceedings(GlueckLeuschel:99:PSI,
 author       = {Robert Gl{\"u}ck and Michael Leuschel},
 year         = {2000},
 title        = {Abstraction-based partial deduction for solving inverse problems: a transformational approach to software verification},
 editor       = {Bj{\o}rner, Dines and Manfred Broy and Alexandre V. Zamulin},
 booktitle    = {Perspectives of System Informatics. Proceedings},
 series       = {LNCS 1755},
 publisher    = {Springer-Verlag},
 pages        = {93--100},
 doi          = {10.1007/3-540-46562-6\_8},
)
@article(Jones:77,
 author       = {Neil D. Jones},
 year         = {1977},
 title        = {A note on linear time simulation of deterministic two-way pushdown automata},
 journal      = {Information Processing Letters},
 volume       = {6},
 number       = {4},
 pages        = {110--112},
 doi          = {10.1016/0020-0190(77)90022-9},
)
@book(Jones:97:complexity,
 author       = {Neil D. Jones},
 year         = {1997},
 title        = {Computability and Complexity: From a Programming Language Perspective},
 series       = {Foundations of Computing},
 publisher    = {MIT Press},
 address      = {Cambridge, Massachusetts},
)
@inproceedings(Klimov:12,
 author       = {Andrei V. Klimov},
 year         = {2012},
 title        = {Solving coverability problem for monotonic counter systems by supercompilation},
 editor       = {Edmund M. Clarke and Irina Virbitskaite and Andrei Voronkov},
 booktitle    = {Perspectives of Systems Informatics. Proceedings},
 series       = {LNCS 7162},
 publisher    = {Springer-Verlag},
 pages        = {193--209},
 doi          = {10.1007/978-3-642-29709-0\_18},
)
@article(KnuMorPra:77,
 author       = {Donald E. Knuth and James H. Morris and Vaughan R. Pratt},
 year         = {1977},
 title        = {Fast pattern matching in strings},
 journal      = {SIAM Journal on Computing},
 volume       = {6},
 number       = {2},
 pages        = {323--350},
 doi          = {10.1137/0206024},
)
@article(Kowalski:79,
 author       = {Robert Kowalski},
 year         = {1979},
 title        = {Algorithm = logic + control},
 journal      = {Communications of the ACM},
 volume       = {22},
 number       = {7},
 pages        = {424--436},
 doi          = {10.1145/359131.359136},
)
@article(LisitsaNemytykh:07,
 author       = {Alexei P. Lisitsa and Andrei P. Nemytykh},
 year         = {2007},
 title        = {Verification as a parameterized testing (experiments with the {SCP4} supercompiler)},
 journal      = {Programming and Computer Software},
 volume       = {33},
 number       = {1},
 pages        = {14--23},
 doi          = {10.1134/S0361768807010033},
)
@article(Mogensen:94,
 author       = {Torben {\AE}. Mogensen},
 year         = {1994},
 title        = {{WORM-2DPDAs}: an extension to {2DPDAs} that can be simulated in linear time},
 journal      = {Information Processing Letters},
 volume       = {52},
 number       = {1},
 pages        = {15--22},
 doi          = {10.1016/0020-0190(94)90134-1},
)
@article(Nepeivoda:16,
 author       = {Antonina N. Nepeivoda},
 year         = {2016},
 title        = {Ping-pong protocols as prefix grammars: modelling 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},
)
@book(Reus:16,
 author       = {Bernhard Reus},
 year         = {2016},
 title        = {Limits of Computation},
 publisher    = {Springer-Verlag},
 doi          = {10.1007/978-3-319-27889-6},
)
@article(RSA:78,
 author       = {Ronald L. Rivest and Adi Shamir and Leonard M. Adleman},
 year         = {1978},
 title        = {A method for obtaining digital signatures and public-key cryptosystems},
 journal      = {Communications of the ACM},
 volume       = {21},
 number       = {2},
 pages        = {120--126},
 doi          = {10.1145/359340.359342},
)
@inproceedings(sorm99:intro,
 author       = {S{\o}rensen, Morten H. and Robert Gl\"uck},
 year         = {1999},
 title        = {Introduction to supercompilation},
 editor       = {John Hatcliff and Torben {\AE}. Mogensen and Peter Thiemann},
 booktitle    = {Partial Evaluation. Practice and Theory},
 series       = {LNCS 1706},
 publisher    = {Springer-Verlag},
 pages        = {246--270},
 doi          = {10.1007/3-540-47018-2\_10},
)
@article(SwiftWarren:12,
 author       = {Terrance Swift and David S. Warren},
 year         = {2012},
 title        = {{XSB}: extending {Prolog} with tabled logic programming},
 journal      = {Theory and Practice of Logic Programming},
 volume       = {12},
 number       = {1-2},
 pages        = {157--187},
 doi          = {10.1017/S1471068411000500},
)
@article(Turchin:86,
 author       = {Valentin F. Turchin},
 year         = {1986},
 title        = {The concept of a supercompiler},
 journal      = {ACM TOPLAS},
 volume       = {8},
 number       = {3},
 pages        = {292--325},
 doi          = {10.1145/5956.5957},
)
@book(WagnerWechsung:86,
 author       = {Klaus Wagner and Gerd Wechsung},
 year         = {1986},
 title        = {Computational Complexity},
 publisher    = {D.\ Reidel Publishing Company},
 address      = {Dordrecht, The Netherlands},
)