Next: About this document ...
Up: Verification via Supercompilation
Previous: Future Work
- 1
- 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.
- 2
- Abstract State Machines:
A Formal Method for Specification and Verification
- 3
-
E.M. Clarke, Grumberg and D. Peled.
Model Checking.
MIT Press, 1999.
- 4
- Giorgio Delzanno. Verification of Consistency Protocols via
Infinite-state Symbolic Model Checking, A Case Study. In
Proc. of FORTE/PSTV, 2000, pp 171-188
- 5
- Giorgio Delzanno,
Constraint-based Verification of Parameterized Cache Coherence Protocols
Formal Methods in System Design 23(3): 257-301, 2003
- 6
- A. P. Ershov. Mixed computation in the class of
recursive program schema. Acta Cybernetica, 4(1), 1978.
- 7
- J.Esparza, Decidability of model checking
of infinite state concurrent systems.
Acta Informatica, 34:85-107, 1997.
- 8
- Y. Futamura and K. Nogi. Generalized partial
computation. In Proceedings of the IFIP TC2
Workshop, pages 133-151. Amsterdam: North-Holland
Publishing Co., 1988.
- 9
- 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.
- 10
- N. D. Jones, C. K. Gomard, and P. Sestoft. Partial
Evaluation and Automatic Program Generation.
Prentice Hall International, 1993, available online
- 11
- 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
- 12
- 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.
- 13
- 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.
- 14
- M. Leuschel. On the Power of Homeomorphic Embedding for Online Termination.
Proceeding of the SAS'98, LNCS 1503, Springer-Verlag,
1998.
- 15
- M.Leuschel, H. Lehmann. Program Specialization,
Inductive Theorem Proving and Infinite State Model Checking,
Invited talk, LOPSTR'03,
Uppsala, 2003, avaialable online
- 16
- 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.
- 17
- Alexei Lisitsa and Andrei Nemytykh, Towards verification via
supercompilation, to appear in Proceedings of COMPSAC'2005, 2005, 2p
- 18
- 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.
- 19
- 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.
- 20
- Andrei P. Nemytykh. Playing on REFAL, In Proc. of
International Workshop on Program Understanding, Novosibirsk-Altay, July 2003.
- 21
- A. P. Nemytykh and V. F. Turchin. The
Supercompiler Scp4: sources, on-line demonstration.
- 22
- S. A. Romanenko. Arity raiser and its use in program
specialization. Proceeding of the ESOP'90, LNCS,
Springer-Verlag, 432:341-360, 1990.
- 23
- 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.
- 24
- 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.
- 25
- 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
- 26
- V. F. Turchin. The concept of a supercompiler. ACM
Transactions on Programming Languages and
Systems, 8:292-325, 1986.
- 27
- V. F. Turchin. Refal-5, Programming Guide and
Reference Manual. Electronic version.
- 28
- V. F. Turchin. Supercompilation: Techniques and
results. Perspectives of System Informatics, LNCS,
Springer-Verlag, 1181:227-248, 1996.
Alexei Lisitsa
2005-07-14