Bernard Elspas
- 1 AMAREL, S. "An approach to heuristic problem solving and theorem prowng in the propositional calculus." In Systems and computer science, Hart and Takasu (Eds.), Univ. Toronto Press, Toronto, Ont., Canada, 1967.Google Scholar
- 2 ANDERSON, l:{. "Completeness results for E- esolution." In Proc. AFIPS 1970 SJCC, Vol. 36, AFIPS Press, Montvale, N.J., 653-656Google Scholar
- 3 ANDREWS, P. B. "Resolution with merging." J A CM 15, 3 (July 1968), 367-381. Google Scholar
- 4 ANDREWS, P. B. "Resolution in type theory." Dept of Mathematics, Carnegie Mellon Univ., Pittsburgh, Pa, 1970Google Scholar
- 5 BURGE, W. H "Provlng the correctness of a compiler." IBM Research Rept RC 2111, Yorktown Heights, N.Y, June 1969Google Scholar
- 6 BURSTALL, R M "Proving properties of programs by structural induction." Computer J. 12, 1 (Feb 1969), 41-48Google Scholar
- 7 CHURCH, A. "The calculi of lambda-conver- SLOE." In Annals of mathematical studies, No. 6, Princeton Umv Press, Princeton, N.J., 1941. Google Scholar
- 8 COOPER, D. C "Program scheme equivalences and second order logic." In Machine ,ntelhgence 4, B. Meltzer and D. Mlchie (Eds.), American Elsevier Publ. Co., New York, 1969, 3-15.Google Scholar
- 9 DARI,INGTON, J. L. "Automatic theorem proving with equality substitution and mathematical induction." In Machine ~ntelligence 3, D. Miehm (Ed.), American Elsevier Publ. Co., New York, 1968, 113-127.Google Scholar
- 10 DAvis, M. Computability and unsolvabiIity McGraw-Hill Book Co , New York, 1958.Google Scholar
- 11 DAvis, M.; AND H. PUTNAM. "A computing procedure for quantification theory." J. ACM 7, 3 (July 1960), 201-215. Google Scholar
- 12 DE BAKKER, J W. "Semantics of programming languages." In Advances ~n znformatwn systems sczence, Vol 2, J. T. Ton (Ed.), Plenum Press, New York, 1969.Google Scholar
- 13 DIJKSTRA, E. W. "A constructive approach to the problem of program correctness " BIT 8, 3 (1968), 174-186.Google Scholar
- 14 DIJKSTRA, E W. "Notes on structured programming." TH Rept 70-WSK-03, 2nd ed., Technische Hogeschool, Eindhoven, The Netherlands, April 1970.Google Scholar
- 15 ELsPAS, B.; M W. GREEN; AND K. N. LEVITT. "Software reliability." Computer 4, 1 (Jan.- Feb. 1971), 21-27Google Scholar
- 16 FLORENTIN, J J. "Language definitmn and computer validation " In Machine ~nteIligence S, D. Michie (Ed.), American Elsevier Publ. Co., New York, 1968, 33-41.Google Scholar
- 17 FLOYD, R W A protocol of an ~maginary program retailer. Preliminary draft, July 1967.Google Scholar
- 18 FLOYD, R. W. "Assigning meanings to programs." In Mathematical aspects of computer science, Vol. 19, J. T. Schwartz (Ed), Amer. Math. Soc , Providence, R.I, 1967, 19-32Google Scholar
- 19 GOLDSTINE, H. H.; AND J. YON NEUMANN "Planning and coding problems for an electronic computer instrument, part 2, vol 1-3." In John yon Neumann collected works, Vol. 5, A. H. Taub (General Ed.), Pergamon Press, New York, 1963, 80-235.Google Scholar
- 20 GooD, D. I. "Toward a man-machine system for proving program correctness " Univ. Texas, TSN-11, Austin, Texas, June 1970; also PhD Thesls, Dept. Computer Sciences, Univ. Wisconsin, Madison, Wlsc, 1970. Google Scholar
- 21 GOVLD, W. E. "A matching procedure for ~-order logic." PhD Thesis, Princeton Univ., Princeton, N.J., 1966.Google Scholar
- 22 GREEN, C. "Application of theorem proving to problem solving." In Proc. Internat. Joznt Conf. on A rhfic~al InteIhgence, D. E. Walker and L. M. Norton (Eds.), Mitre Corp , Bedford, Mass., 1969, 219-239.Google Scholar
- 23 GREF~N, C. "The application of theorem proving to question-answering systems." Tech. Note 8, SRI Project 7494, Stanford Research Inst., Menlo Park, Calif., June 1969.Google Scholar
- 24 GREEN, C. "Theorem proving by resolution as a basis for question-answering systems." In Machine intelhgence ~4, B. Meltzer and D. Michie (Eds.), Edinburgh Univ. Press, Edinburgh, Scotland, 1969, 183-205Google Scholar
- 25 GREEN, M. W.; B. ELs~As; AND K. N. LEVITT. "Translation of recursive schemas into labelstack flow-chart schemas." Prehminary draft, Stanford Research Inst., Menlo Park, Calif., June 1971.Google Scholar
- 26 HANSEN, P. B. "The nucleus of a multiprogramming system." Comm. ACM 13, 4 (April 1970), 238-241. Google Scholar
- 27 HAYES, P. J. "A machine-oriented formulation of the extended functmnal calculus " Stanford Artificial Intelligence Project, Memo 62; also appeared as Metamathematics Unit Report, Univ. Edinburgh, Scotland, 1969.Google Scholar
- 28 HEaBR.~ND, J. "Recherches sur la th~orie de la d6monstration." Travaux de la Societ6 des Sciences et des Lettres de Varsovm, Classe IiI, No. 33, Paris, 1930.Google Scholar
- 29 HEWlTT, C. "More comparative schematology." Artificial Intelligence Memo No. 207, Project MAC, MIT, Cambridge, Mass., Aug. 1970.Google Scholar
- 30 HOARE, C. A. R. "An axiomatic basis for computer programming " Comm. A CM 12, 10 (Oct. 1969), 576-580, 583. Google Scholar
- 31 IANOV, Y. I. "The logical schemes of algorithms " In Problems of cybernetics, Vol 1, Translated from the Russmn by Nadler, Grifi~ths, Kms, and Muir, Pergamon Press, New York, 1960, 82-140Google Scholar
- 32 KAPLAN, D. M. "Proving things about programs." Presented at ~th Annual Pmnceton Conf. on Information Science and Systems, Princeton Univ, March 1970.Google Scholar
- 33 KING, J. C. "A program verifier." Unpublished research, PhD Thesis, Carnegie-Mellon Univ., Pittsburgh, Pa, 1969. Google Scholar
- 34 KING, J. C ; AND R W. FLOYD. "An interpretation oriented theorem prover over integers." }n Proc. 2nd Annual A CM Symposium on Theory of Computing, ACM, New York, 1970, 169-179. Google Scholar
- 35 KLEENE, S. C Introductwn to metamathemattes, D. Van Nostrand Co., Inc, Princeton, N.J., 1952.Google Scholar
- 36 KONIG, D. Theome der endlichen ur~d unendl~chen Graphen Chelsea Publ. Co., Bronx, N Y, 1950, 81Google Scholar
- 37 LANDIN, P. J ; AND ~. M. BURSTALL "Programs and their proofs: an algebraic approach." In Machzne ~ntell, gence 4, B. Meltzer and D. Mlchie (Eds.), American Elsevmr Publ. Co, New York, 1969Google Scholar
- 38 LEAVENWORTH, B. Review of paper by P Naur {"Programming by action clusters " BIT 9, 3 (1969), 250-258}. Computing Reviews ll, 7 (July 1970), Rev. 19,420Google Scholar
- 39 LONDON, }~. L. "Computer programs can be proved correct " In Proc ~th Systems Symposium-Formal Systems and Non-Numemcal Problem Solwng by Computers, held at Case Western Reserve Univ., November 1968, R. B. Banerji and M D. Mesarovic (Eds.), Springer Verlag, New York, 1970, 281-302.Google Scholar
- 40 LONDON, t{. L. "Proof of algorithms, a new kind of certification (certification of algorithm 245, TaE~soaT 3) " Comm. ACM 13, 6 (June 1970), 371-373 Google Scholar
- 41 LONDON, ~. L "Bibliography on proving the correctness of computer programs." In Machine ~ntellzgence 5, B Meltzer and D Michie (Eds.), American Elsevier Publ. Co., New York, 1970, 569-580.Google Scholar
- 42 LONDON, ~. L. "Software reliability through proving programs correct " Publ 71C 6-C, IEEE Computer Society, New York, March 1971Google Scholar
- 43 LONDON, }:{. L.; AND J. H. HA.LTON. "Proofs of algorithms for asymptotic series " Computer Sciences Tech Rept No. 54A, Univ Wisconsin, Madison, Wise , May 1969.Google Scholar
- 44 LOVELAND, D. A "A linear format for resolution " Proc Symposium on Automatw Deductwn, Inst de Recherche d'Informatique et d'Automatique, Versailles, France, Dec. 1968 In Lecture notes ~n mathematzcs, No 125, Springer Verlag, New York, 1970.Google Scholar
- 45 LUCKHAM, }_). "Some tree-paring strategies for theorem-proving " In Machine ,ntelligence 3, D. Michie (Ed), American Elsevier Publ. Co., York, 1968, 95-112.Google Scholar
- 46 LUCKUa~, D "Refinement theorems in resolution theory " Proc. Symposium on Automatzc Deductwn, Inst. de Recherche d'Informatique et d'Automa~lque, Versailles, France, Dec. 1968. In Lecture notes ~n mathematics, No. 125, Springer Verlag, New York 1970; also in Stunford Artificial Intelhgence Project Memo AI-81, 1969Google Scholar
- 47 LUCKHAM, D. C.; D. M. R. PAR~; AND M S. PATERSOn. "On formalized computer programs " J. Computer & System Sciences 4, 3 (June 1970), 220-249.Google Scholar
- 48 M~NNA, Z. "Froperties of programs and the first-order predicate calculus " j ACM 16, 2 (April 1969), 244-255 Google Scholar
- 49 MANNA, Z. "The correctness of programs." J. Compu~,er & System Sciences 3, 2 (May 1969), 119-127.Google Scholar
- 50 MANNA, Z "Second-order mathematical theory of computation." In Proc. 2nd Annual ACM Symposium on Theory of Computing, ACM, New York, 1970, 158-168. Google Scholar
- 51 MANNA, Z.; AND J. MCCARTHY "Properties of programs and partial functmn logic " In Macine mtelhgence 5, B. Meltzer and D. Mlchie (Eds.), American Elsevier Publ .Co., New York, 1970, 27-37Google Scholar
- 52 MANNA, Z.; AND A PNUELI "The validity problem of the 91-function." Artificial Intelligence Memo No 68, Stanford Univ., Stanford, Calif., Aug. 1968Google Scholar
- 53 MANNA, Z.; AND A. PNUELI, "Formahzation of properties of recursively defined functions." In Proc. A CM Symposium on Theory of Computing, ACM, New York, 1969, 201-210. Google Scholar
- 54 MANNA, Z.; AND A PNUELI, "Formalization of properties of functional programs." J. ACM 17, 3 (July 1970), 555-569 Google Scholar
- 55 M~kblNA, Z ; AND R. J. W~LDINGER, "Towards automatic program synthesis." Comm. ACM 14, 3 (March 1971), 151-165. Google Scholar
- 56 MCCARTHY, J. "A basis for a mathematical theory of computation." In Computer programm~ng and formal systems, P Braffort and D. Hirschberg (Eds.), North-Holland Publ. Co., Amsterdam, 1963, 33-70; also ia Proc. Western Joint Computer Conf, Vol. 19, Spartan Books, New York, 1961, 225-238Google Scholar
- 57 McCAaTHY, J "Towards a mathematical science of computation " In Proc. IFIP Cong. 62, C. M Popplewell (Ed.), North-Holland Publ. Co , Amsterdam, 1963, 21-28.Google Scholar
- 58 MCCARTHY, J ; AND J A. PAINTER "Correctness of a compiler for arithmetic expressmns." In Mathematical aspects of computer science, Vol. 19, J T. Schwartz (Ed), Amer. Math Soc , Providence, R I , 1967, 33-41Google Scholar
- 59 MEJ~ZER, B. "Theorem-proving for computers some results on resolution and renaming." Computer J 8, 4 (Jan. 1956), 341-343.Google Scholar
- 60 MENDELSON, E Introduc~wn to mathematical logic V~n Nostrand Co., Princeton Univ. Press, Princeton, N.J., 1964. Google Scholar
- 61 Mo~s, J. B., J~. "E-resolutmn: extension of resolutmn to include the equality relation." In Proc. Internatl. Joint Conf. on Artificial Intelligence, D. E. Walker and L M. Norton (Eds), The Mitre Corp , Bedford, Mass., 1969, 287-294Google Scholar
- 62 NAun, P. "Proof of algorithms by general snapshots " BIT 6, 4 (1966), 310-316.Google Scholar
- 63 NAun, P. "Programming by action clusters." BIT 9, 3 (1969), 250-258.Google Scholar
- 64 NEWELL, A.; J C SH~W; AND H. A. SIMON. "Empirical explorations of the logic theory machine a case study in heuristic " In Proc. Western Joint Computer Conf , Vol. 11, Spartan Books, New York, 1957, 218-230.Google Scholar
- 65 PARK, D. "F1xpomt induction and proofs of program properties " In Machine ~ntelhgence 5, B Meltzer and D Michie (Eds), American Elsevier Publ. Co , New York, 1969, 59-78.Google Scholar
- 66 PATERSON, M S. "Equivalence problems in a model of computation " PhD Thesis, Cambridge Univ., Cambridge, England, Aug. 1967.Google Scholar
- 67 PATERSON, M S ; AND C E. HEWITT. "Comparative schematology " In Record o~ the Prosect MAC Conf on Concurrent Systems and Parallel Computatwn, ACM:, New York, 1970, 119-127Google Scholar
- 68 PI~AWlTZ, D. "An improved proof procedure " Theorm 26, (1980), 102-139.Google Scholar
- 69 ROBINSON, G ;AND L. WoN. "Paramodulation and theorem-proving ~n first-order theories with equality " In Machine zntelhgence 4, B. Meltzer and D. Michm (Eds.), American Elsevier Publ. Co, New York, 1969, 135-150.Google Scholar
- 70 ROBINSON, J A. "A machine-oriented logic based on the resolution principle " J. ACM 12, 1 (Jan 1965), 23-41 Google Scholar
- 71 ROBINSON, J. A. "Automatic deduction with hyper-resolutlon " Internatl J. Computer Math 1, (1965), 227-234Google Scholar
- 72 ROBINSON, J A. "Mechanizing htgher-order logic " In Machine ~ntelhgence 4, B Meltzer and D Mlchle (Eds.), Amerman Elsevier Publ. Co., New York, 1969, 151-170Google Scholar
- 73 ROGERS, H Theory of recurswe functzons and eOectwe computab~hty. McGraw Hill Book Co , New York, 1967. Google Scholar
- 74 RULXFSON, J. F, R. J. WALDINGER, AND J. DERKSEN "A language for wmting problemsolving programs " Presented at IFIP Cong. 1971, Ljubljana, Yugoslavia, Aug 1971, North- Holland Publ. Co, Amsterdam, 1972.Google Scholar
- 75 RUSSELL, B;AND A N WHITEHEAD Pr~ncipia mathematzca, Vo{s 1-3. University Press, Cambridge, England, 1925-7 (2d ed.).Google Scholar
- 76 RUTLEDGE, J. D. "On Ianov's program schemata " J A CM 11, 1 (Jan. 1964), 1-9. Google Scholar
- 77 SIMON, H A "Experiments with a heuristic compiler." J. ACM 10, 4 (Oct. 1963), 493-506. Google Scholar
- 78 SLAGLP., J. R. "Automatic theorem-proving with renamable and semantic resolution." J. A CM 14, 4 (Oct 1967), 687-697. Google Scholar
- 79 STRONG, H. R, JR. "Translating recursion equations into flow charts " In Proc 2nd Annual A CM Symposium on Theory of Computing, ACM, New York, 1970, 184-197. Google Scholar
- 80 WALDINGER, R J "Constructing programs automatically using theorem proving." PhD Thesis, Carnegie-Mellon Univ., Pittsburgh, Pa., 1969Google Scholar
- 81 WALDINGER, R J.; AND R. C. T. LEE. "PRow: a step toward automatic program writing " In Proc Internat Joint Conf. on Art~ficzal Intelhgence, D. E Walker and L. M Norton (Eds), Mitre Corp, Bedford, Mass., 1969, 241-252.Google Scholar
- 82 WANG, H "Toward mechanical m~thematics." IBM d. R & D 4, (1960), 2-22.Google Scholar
- 83 WENSbEY, J. H. "A class of non-analytical iteratlve processes " Computer J. 1, (1958), 163-167Google Scholar
- 84 Wos, L ; G. A ROBINSON; AND D. F. CARSON. "Effacmncy and completeness of the set of support strategy m theorem proving." J. ACM 12, 4 (Oct. 1965), 536-541 Google Scholar
- 85 Wos, L ; D. F. CARSON; AND G. A ROBINSON. "The unit preference strategy in theorem proving" In Proc. I964 FJCC, Vol 26, Pt 1, Spartan Books, New York, 615-621 Google Scholar
- 86 YATES, R, B RAPHAEL; AND T. P HART. "Resolution graphs." Artificial Intelligence Group, Stanford Research Inst. Tech. Note 24, Menlo Park, Callf, 1970Google Scholar
Recommendations
Test data as an aid in proving program correctness
Proofs of program correctness tend to be long and tedious, whereas testing, though useful in detecting errors, usually does not guarantee correctness. This paper introduces a technique whereby test data can be used in proving program correctness. In ...
Test data as an aid in proving program correctness
POPL '76: Proceedings of the 3rd ACM SIGACT-SIGPLAN symposium on Principles on programming languagesProofs of program correctness tend to be long and tedious whereas testing, though useful in detecting errors, usually does not guarantee correctness. This paper introduces a technique whereby test data can be used in proving program correctness. In ...
Proving Correctness of an Efficient Abstraction for Interrupt Handling
This paper presents an approach to the efficient abstraction of interrupt handling in microcontroller systems. Such systems usually operate in uncertain environments, giving rise to a high degree of nondeterminism in the corresponding formal models, ...
Comments