References

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