next up previous
Next: About this document ... Up: Verification via Supercompilation Previous: Future Work


S. Abramov. Metacomputation and program testing. In: Proc. of 1st International Workshop on Automated and Algorithmic Debugging (AAEBUG'93), pp. 121-135, Linkoping Univ., Sweden, 3-5 May, 1993.

Abstract State Machines: A Formal Method for Specification and Verification

E.M. Clarke, Grumberg and D. Peled.
Model Checking.
MIT Press, 1999.

Giorgio Delzanno. Verification of Consistency Protocols via Infinite-state Symbolic Model Checking, A Case Study. In Proc. of FORTE/PSTV, 2000, pp 171-188

Giorgio Delzanno, Constraint-based Verification of Parameterized Cache Coherence Protocols Formal Methods in System Design 23(3): 257-301, 2003

A. P. Ershov. Mixed computation in the class of recursive program schema. Acta Cybernetica, 4(1), 1978.

J.Esparza, Decidability of model checking of infinite state concurrent systems. Acta Informatica, 34:85-107, 1997.

Y. Futamura and K. Nogi. Generalized partial computation. In Proceedings of the IFIP TC2 Workshop, pages 133-151. Amsterdam: North-Holland Publishing Co., 1988.

Robert Glück and Michael Leuschel, Abstraction-based partial deduction for solving inverse problems - a transformational approach to software verification. In Proceedings of Systems Informatics, LNCS 1755, pages 93-100, Novosibirsk, Russia, 1999. Springer-Verlag.

N. D. Jones, C. K. Gomard, and P. Sestoft. Partial Evaluation and Automatic Program Generation. Prentice Hall International, 1993, available online

Andy King and Lunjin Lu Forward versus Backward Verification of Logic Programs. In Catuscia Palamidessi, editor, International Conference on Logic Programming, volume 2916 of Lecture Notes in Computer Science, pages 315-330. Springer-Verlag, December 2003

A. V. Korlyukov and A. P. Nemytykh. Supercompilation of Double Interpretation. (How One Hour of the Machine's Time Can Be Turned to One Second), available online , 2002.

M. Leuschel and B. Martens. Global Control for Partial Deduction through Characteristic Atoms and Global Trees. Proceeding of the PEPM'96, LNCS 1110, Springer-Verlag, 1996.

M. Leuschel. On the Power of Homeomorphic Embedding for Online Termination. Proceeding of the SAS'98, LNCS 1503, Springer-Verlag, 1998.

M.Leuschel, H. Lehmann. Program Specialization, Inductive Theorem Proving and Infinite State Model Checking, Invited talk, LOPSTR'03, Uppsala, 2003, avaialable online

M.Leuschel, H. Lehmann, Solving coverability problems of Petri nets by partial deduction. In Proc. 2nd Int. ACM SIGPLAN Conf. on Principles and Practice of Declarative Programming (PPDP'2000), Montreal, Canada, pp 268-279, 2000.

Alexei Lisitsa and Andrei Nemytykh, Towards verification via supercompilation, to appear in Proceedings of COMPSAC'2005, 2005, 2p

A. P. Nemytykh. A Note on Elimination of Simplest Recursions. In Proceedings of the ACM SIGPLAN Asian Symposium on Partial Evaluation and Semantics-Based Program Manipulation, 138-146. ACM Press, 2002.

Nemytykh A.P., The Supercompiler SCP4: General Structure. Extended Abstract. In Proc. of Perspectives of System Informatics, Lecture Notes in Computer Science, 2890 (2003), pp: 162-170.

Andrei P. Nemytykh. Playing on REFAL, In Proc. of International Workshop on Program Understanding, Novosibirsk-Altay, July 2003.

A. P. Nemytykh and V. F. Turchin. The Supercompiler Scp4: sources, on-line demonstration.

S. A. Romanenko. Arity raiser and its use in program specialization. Proceeding of the ESOP'90, LNCS, Springer-Verlag, 432:341-360, 1990.

D. Sands, Proving the correctness of recursion-based automatic program transformation. In Theory and Practice of Software Development, volume 915 of LNCS, pp 681-695, 1995.

M. H. Sorensen and R. Glueck. An algorithm of generalization in positive supercompilation. In Logic Programming: Proceedings of the 1995 International Symposium, pages 486-479. MIT Press, 1995.

Morten H. Sørensen and Robert Glück. Introduction to Supercompilation. Partial Evaluation - Practice and Theory, DIKU 1998 International Summer School. June 1998, available online

V. F. Turchin. The concept of a supercompiler. ACM Transactions on Programming Languages and Systems, 8:292-325, 1986.

V. F. Turchin. Refal-5, Programming Guide and Reference Manual. Electronic version.

V. F. Turchin. Supercompilation: Techniques and results. Perspectives of System Informatics, LNCS, Springer-Verlag, 1181:227-248, 1996.

Alexei Lisitsa 2005-07-14