{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,3,31]],"date-time":"2022-03-31T11:00:24Z","timestamp":1648724424002},"reference-count":18,"publisher":"EDP Sciences","issue":"1","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["RAIRO. Inform. th\u00e9or."],"published-print":{"date-parts":[[1983]]},"DOI":"10.1051\/ita\/1983170100551","type":"journal-article","created":{"date-parts":[[2017,2,6]],"date-time":"2017-02-06T10:34:00Z","timestamp":1486377240000},"page":"55-70","source":"Crossref","is-referenced-by-count":2,"title":["Top-down mathematical semantics and symbolic execution"],"prefix":"10.1051","volume":"17","author":[{"given":"G.","family":"L\u00e9vi","sequence":"first","affiliation":[]},{"given":"A. M.","family":"Pegna","sequence":"additional","affiliation":[]}],"member":"250","published-online":{"date-parts":[[2011,1,8]]},"reference":[{"key":"R1","unstructured":"1. AMBRIOLA V. and LEVI G., The equational language TEL: formal semantics and implementation, IEI Internal Report (in preparation)."},{"key":"R2","unstructured":"2. ASIRELLI P., DEGANO P., LEVI G., MARTELLI A., MONTANARI U., PACINI G., SIROVICH F. and TURINI F., A flexible environment for program development based on a symbolic interpreter, Proc. 4th Int'1 Conf. on Software Engineering, 1979, p. 251-263."},{"key":"R3","doi-asserted-by":"crossref","unstructured":"3. BOYER R. S., ELSPAS B. and LEVITT K. N., SELECT. A formal system for testing and debugging programs by symbolic execution. Proc. Int'1 Conf. on Reliable Software, 1975, p. 234-245.","DOI":"10.1145\/390016.808445"},{"key":"R4","doi-asserted-by":"crossref","unstructured":"4. BOYER R. S. and MOORE J. S., Proving theorems about LISP functions, J. ACM 22, 1975, p. 129-144.4950810338.68014","DOI":"10.1145\/321864.321875"},{"key":"R5","unstructured":"5. BOYER R. S. and MOORE J. S., A lemma driven automatic theorem prover for recursive function theory, Proc. 5th Int'1 Joint Conf. on Artificial Intelligence, 1977, p. 511-519."},{"key":"R6","unstructured":"6. BURSTALL R. M., Program proof, program transformation, program synthesis for recursive programs. Rivista di Informatica, vol. 7, Suppl. 1, 1977, p. 25-43."},{"key":"R7","doi-asserted-by":"crossref","unstructured":"7. BURSTALL R. M. and DARLINGTON J., A transformation system for developing recursive programs. J. ACM 24, 1977, p. 44-67.4518160343.68014","DOI":"10.1145\/321992.321996"},{"key":"R8","unstructured":"8. DEUTSCH L. P., An interactive program verifier - Ph. D. - dissertation, Dept. of Comp. Sci., Univ. of California, Berkeley (May 1973)."},{"key":"R9","unstructured":"9. GOGUEN J. A., Abstract errors for abstract data types. Formal Description of Programming Concepts, E. J. Neuhold Ed., North-Holland, 1978, p. 491-522.5379180373.68024"},{"key":"R10","doi-asserted-by":"crossref","unstructured":"10. KING J. C., A new approach to program testing. Proc. Int'l Conf. on Reliable Software, 1975, p. 228-233.","DOI":"10.1145\/800027.808444"},{"key":"R11","doi-asserted-by":"crossref","unstructured":"11. KING J. C., Symbolic execution and program testing. Comm. ACM 19, 1976, p. 385-395.4185020329.68018","DOI":"10.1145\/360248.360252"},{"key":"R12","doi-asserted-by":"crossref","unstructured":"12. LEVI G. and SIROVICH F., 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.3915600325.68008","DOI":"10.1007\/3-540-07389-2_211"},{"key":"R13","doi-asserted-by":"crossref","unstructured":"13. LONDON R. L. and MUSSER D. R., The application of a symbolic mathematical System to program verification, Proc. ACM Annual Conf., 1974, p. 265-273.","DOI":"10.1145\/800182.810412"},{"key":"R14","doi-asserted-by":"crossref","unstructured":"14. MORRIS J. A. and WEGBREIT B., Subgoal induction, Comm. ACM 20, 1977, p. 209-222.4458890349.68007","DOI":"10.1145\/359461.359466"},{"key":"R15","unstructured":"15. NIVAT M., On the interpretation of recursive polyadic program schemes, Symposia Mathematica, vol. 15, 1975, p. 255-281.3915630346.68041"},{"key":"R16","unstructured":"16. PEGNA A. M., Una caratterizzazione della semantica dei linguaggi programmativi basata sulla valuatazione simbolica, Proc. AICA, 77, 3 1977, p. 93-99."},{"key":"R17","unstructured":"17. TOPOR R. W., Interactive program verification using virtual programs, Ph. D. dissertation, Dept. of Artificial Intelligence, Univ. of Edinburgh (February, 1975)."},{"key":"R18","doi-asserted-by":"crossref","unstructured":"18. VAN EMDEN M. H. and KOWALSKI R. A., The semantics of predicate logic as a programming language, J. ACM 23, 1976, p. 733-742.4555090339.68004","DOI":"10.1145\/321978.321991"}],"container-title":["RAIRO. Informatique th\u00e9orique"],"original-title":[],"link":[{"URL":"http:\/\/www.rairo-ita.org\/10.1051\/ita\/1983170100551\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,9,18]],"date-time":"2019-09-18T05:33:41Z","timestamp":1568784821000},"score":1,"resource":{"primary":{"URL":"http:\/\/www.rairo-ita.org\/10.1051\/ita\/1983170100551"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1983]]},"references-count":18,"journal-issue":{"issue":"1"},"alternative-id":["ita1983170100551"],"URL":"https:\/\/doi.org\/10.1051\/ita\/1983170100551","relation":{},"ISSN":["0399-0540"],"issn-type":[{"value":"0399-0540","type":"print"}],"subject":[],"published":{"date-parts":[[1983]]}}}