Top-down mathematical semantics and symbolic execution

G. Lévi; A. M. Pegna

RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications (1983)

  • Volume: 17, Issue: 1, page 55-70
  • ISSN: 0988-3754

How to cite

top

Lévi, G., and Pegna, A. M.. "Top-down mathematical semantics and symbolic execution." RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications 17.1 (1983): 55-70. <http://eudml.org/doc/92178>.

@article{Lévi1983,
author = {Lévi, G., Pegna, A. M.},
journal = {RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications},
keywords = {formal semantics; equational language},
language = {eng},
number = {1},
pages = {55-70},
publisher = {EDP-Sciences},
title = {Top-down mathematical semantics and symbolic execution},
url = {http://eudml.org/doc/92178},
volume = {17},
year = {1983},
}

TY - JOUR
AU - Lévi, G.
AU - Pegna, A. M.
TI - Top-down mathematical semantics and symbolic execution
JO - RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications
PY - 1983
PB - EDP-Sciences
VL - 17
IS - 1
SP - 55
EP - 70
LA - eng
KW - formal semantics; equational language
UR - http://eudml.org/doc/92178
ER -

References

top
  1. 1. V. AMBRIOLA and G. LEVI, The equational language TEL: formal semantics and implementation, IEI Internal Report (in preparation). 
  2. 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. 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. 4. R. S. BOYER and J. S. MOORE, Proving theorems about LISP functions, J. ACM 22, 1975, p. 129-144. Zbl0338.68014MR495081
  5. 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. 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. 7. R. M. BURSTALL and J. DARLINGTON, A transformation system for developing recursive programs. J. ACM 24, 1977, p. 44-67. Zbl0343.68014MR451816
  8. 8. L. P. DEUTSCH, An interactive program verifier - Ph. D. - dissertation, Dept. of Comp. Sci., Univ. of California, Berkeley (May 1973). 
  9. 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. Zbl0373.68024MR537918
  10. 10. J. C. KING, A new approach to program testing. Proc. Int'l Conf. on Reliable Software, 1975, p. 228-233. 
  11. 11. J. C. KING, Symbolic execution and program testing. Comm. ACM 19, 1976, p. 385-395. Zbl0329.68018MR418502
  12. 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. Zbl0325.68008MR391560
  13. 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. 14. J. A. MORRIS and B. WEGBREIT, Subgoal induction, Comm. ACM 20, 1977, p. 209-222. Zbl0349.68007MR445889
  15. 15. M. NIVAT, On the interpretation of recursive polyadic program schemes, Symposia Mathematica, vol. 15, 1975, p. 255-281. Zbl0346.68041MR391563
  16. 16. A. M. PEGNA, Una caratterizzazione della semantica dei linguaggi programmativi basata sulla valuatazione simbolica, Proc. AICA, 77, 3 1977, p. 93-99. 
  17. 17. R. W. TOPOR, Interactive program verification using virtual programs, Ph. D. dissertation, Dept. of Artificial Intelligence, Univ. of Edinburgh (February, 1975). 
  18. 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. Zbl0339.68004MR455509

NotesEmbed ?

top

You must be logged in to post comments.

To embed these notes on your page include the following JavaScript code on your page where you want the notes to appear.

Only the controls for the widget will be shown in your chosen language. Notes will be shown in their authored language.

Tells the widget how many notes to show per page. You can cycle through additional notes using the next and previous controls.

    
                

                
Note: Best practice suggests putting the JavaScript code just before the closing </body> tag.