References

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