Top-down mathematical semantics and symbolic execution
Lévi, G. ; Pegna, A. M.
RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications, Tome 17 (1983), p. 55-70 / Harvested from Numdam
Access to full text
Full (PDF)
Full (DJVU)
Publié le : 1983-01-01
@article{ITA_1983__17_1_55_0,
     author = {L\'evi, G. and Pegna, A. M.},
     title = {Top-down mathematical semantics and symbolic execution},
     journal = {RAIRO - Theoretical Informatics and Applications - Informatique Th\'eorique et Applications},
     volume = {17},
     year = {1983},
     pages = {55-70},
     mrnumber = {701988},
     zbl = {0512.68067},
     language = {en},
     url = {http://dml.mathdoc.fr/item/ITA_1983__17_1_55_0}
}

Lévi, G.; Pegna, A. M. Top-down mathematical semantics and symbolic execution. RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications, Tome 17 (1983) pp. 55-70. http://gdmltest.u-ga.fr/item/ITA_1983__17_1_55_0/

1. V. Ambriola and G. Levi, The equational language TEL: formal semantics and implementation, IEI Internal Report (in preparation).

2. P. Asirelli, P. Degano, G. Levi, A. Martelli, U. Montanari, G. Pacini, F. Sirovich and F. Turini, A flexible environment for program development based on a symbolic interpreter, Proc. 4th Int'1 Conf. on Software Engineering, 1979, p. 251-263.

3. R. S. Boyer, B. Elspas and K. N. Levitt, SELECT. A formal system for testing and debugging programs by symbolic execution. Proc. Int'1 Conf. on Reliable Software, 1975, p. 234-245.

4. R. S. Boyer and J. S. Moore, Proving theorems about LISP functions, J. ACM 22, 1975, p. 129-144. | MR 495081 | Zbl 0338.68014

5. R. S. Boyer and J. S. Moore, A lemma driven automatic theorem prover for recursive function theory, Proc. 5th Int'1 Joint Conf. on Artificial Intelligence, 1977, p. 511-519.

6. R. M. Burstall, Program proof, program transformation, program synthesis for recursive programs. Rivista di Informatica, vol. 7, Suppl. 1, 1977, p. 25-43.

7. R. M. Burstall and J. Darlington, A transformation system for developing recursive programs. J. ACM 24, 1977, p. 44-67. | MR 451816 | Zbl 0343.68014

8. L. P. Deutsch, An interactive program verifier - Ph. D. - dissertation, Dept. of Comp. Sci., Univ. of California, Berkeley (May 1973).

9. J. A. Goguen, Abstract errors for abstract data types. Formal Description of Programming Concepts, E. J. Neuhold Ed., North-Holland, 1978, p. 491-522. | MR 537918 | Zbl 0373.68024

10. J. C. King, A new approach to program testing. Proc. Int'l Conf. on Reliable Software, 1975, p. 228-233.

11. J. C. King, Symbolic execution and program testing. Comm. ACM 19, 1976, p. 385-395. | MR 418502 | Zbl 0329.68018

12. G. Levi and F. Sirovich, Proving program properties, symbolic evaluation and logical procedural semantics. Mathematical Foundations of Computer Science 1975. Lecture Notes in Computer Science, Springer Verlag, 1975, p. 294-301. | MR 391560 | Zbl 0325.68008

13. R. L. London and D. R. Musser, The application of a symbolic mathematical System to program verification, Proc. ACM Annual Conf., 1974, p. 265-273.

14. J. A. Morris and B. Wegbreit, Subgoal induction, Comm. ACM 20, 1977, p. 209-222. | MR 445889 | Zbl 0349.68007

15. M. Nivat, On the interpretation of recursive polyadic program schemes, Symposia Mathematica, vol. 15, 1975, p. 255-281. | MR 391563 | Zbl 0346.68041

16. A. M. Pegna, Una caratterizzazione della semantica dei linguaggi programmativi basata sulla valuatazione simbolica, Proc. AICA, 77, 3 1977, p. 93-99.

17. R. W. Topor, Interactive program verification using virtual programs, Ph. D. dissertation, Dept. of Artificial Intelligence, Univ. of Edinburgh (February, 1975).

18. M. H. Van Emden and R. A. Kowalski, The semantics of predicate logic as a programming language, J. ACM 23, 1976, p. 733-742. | MR 455509 | Zbl 0339.68004