article

Free access

An Assessment of Techniques for Proving Program Correctness

Authors:

Bernard Elspas,

Karl N. Levitt,

Richard J. Waldinger,

Abraham WaksmanAuthors Info & Claims

ACM Computing Surveys (CSUR), Volume 4, Issue 2

Pages 97 - 147

https://doi.org/10.1145/356599.356602

Published: 01 June 1972 Publication History

PDF eReader

References

[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-656

Google Scholar

[3]

ANDREWS, P. B. "Resolution with merging." J A CM 15, 3 (July 1968), 367-381.

Crossref

Google Scholar

[4]

ANDREWS, P. B. "Resolution in type theory." Dept of Mathematics, Carnegie Mellon Univ., Pittsburgh, Pa, 1970

Google Scholar

[5]

BURGE, W. H "Provlng the correctness of a compiler." IBM Research Rept RC 2111, Yorktown Heights, N.Y, June 1969

Google Scholar

[6]

BURSTALL, R M "Proving properties of programs by structural induction." Computer J. 12, 1 (Feb 1969), 41-48

Google Scholar

[7]

CHURCH, A. "The calculi of lambda-conver- SLOE." In Annals of mathematical studies, No. 6, Princeton Umv Press, Princeton, N.J., 1941.

Crossref

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.

Crossref

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-27

Google 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-32

Google 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.

Crossref

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-205

Google 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.

Crossref

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.

Crossref

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-140

Google 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.

Crossref

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.

Crossref

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, 81

Google 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, 1969

Google 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,420

Google 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

Crossref

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 1971

Google 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, 1969

Google 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

Crossref

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.

Crossref

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-37

Google Scholar

[52]

MANNA, Z.; AND A PNUELI "The validity problem of the 91-function." Artificial Intelligence Memo No 68, Stanford Univ., Stanford, Calif., Aug. 1968

Google 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.

Crossref

Google Scholar

[54]

MANNA, Z.; AND A PNUELI, "Formalization of properties of functional programs." J. ACM 17, 3 (July 1970), 555-569

Crossref

Google Scholar

[55]

M~kblNA, Z ; AND R. J. W~LDINGER, "Towards automatic program synthesis." Comm. ACM 14, 3 (March 1971), 151-165.

Crossref

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-238

Google 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-41

Google 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.

Crossref

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-294

Google 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-127

Google 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

Crossref

Google Scholar

[71]

ROBINSON, J. A. "Automatic deduction with hyper-resolutlon " Internatl J. Computer Math 1, (1965), 227-234

Google 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-170

Google Scholar

[73]

ROGERS, H Theory of recurswe functzons and eOectwe computab~hty. McGraw Hill Book Co, New York, 1967.

Crossref

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.

Crossref

Google Scholar

[77]

SIMON, H A "Experiments with a heuristic compiler." J. ACM 10, 4 (Oct. 1963), 493-506.

Crossref

Google Scholar

[78]

SLAGLP., J. R. "Automatic theorem-proving with renamable and semantic resolution." J. A CM 14, 4 (Oct 1967), 687-697.

Crossref

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.

Crossref

Google Scholar

[80]

WALDINGER, R J "Constructing programs automatically using theorem proving." PhD Thesis, Carnegie-Mellon Univ., Pittsburgh, Pa., 1969

Google 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-167

Google 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

Crossref

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

Crossref

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, 1970

Google Scholar

Cited By

View all

Müller PShankar N(2021)The First Fifteen Years of the Verified Software ProjectTheories of Programming10.1145/3477355.3477362(93-124)Online publication date: 4-Oct-2021
https://dl.acm.org/doi/10.1145/3477355.3477362
Lucas SGutiérrez R(2018)Automatic Synthesis of Logical Models for Order-Sorted First-Order TheoriesJournal of Automated Reasoning10.1007/s10817-017-9419-360:4(465-501)Online publication date: 1-Apr-2018
https://dl.acm.org/doi/10.1007/s10817-017-9419-3
Visser WBjørner NShankar NHerbsleb JDwyer MHerbsleb J(2014)Software engineering and automated deductionFuture of Software Engineering Proceedings10.1145/2593882.2593899(155-166)Online publication date: 31-May-2014
https://dl.acm.org/doi/10.1145/2593882.2593899
Show More Cited By

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 languages

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 ...
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

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

ACM Computing Surveys Volume 4, Issue 2

June 1972

82 pages

ISSN:0360-0300

EISSN:1557-7341

DOI:10.1145/356599

Issue’s Table of Contents

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 01 June 1972

Published in CSUR Volume 4, Issue 2

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

151
Total Citations
View Citations
1,572
Total Downloads

Downloads (Last 12 months)126
Downloads (Last 6 weeks)16

Reflects downloads up to 11 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

View all

Müller PShankar N(2021)The First Fifteen Years of the Verified Software ProjectTheories of Programming10.1145/3477355.3477362(93-124)Online publication date: 4-Oct-2021
https://dl.acm.org/doi/10.1145/3477355.3477362
Lucas SGutiérrez R(2018)Automatic Synthesis of Logical Models for Order-Sorted First-Order TheoriesJournal of Automated Reasoning10.1007/s10817-017-9419-360:4(465-501)Online publication date: 1-Apr-2018
https://dl.acm.org/doi/10.1007/s10817-017-9419-3
Visser WBjørner NShankar NHerbsleb JDwyer MHerbsleb J(2014)Software engineering and automated deductionFuture of Software Engineering Proceedings10.1145/2593882.2593899(155-166)Online publication date: 31-May-2014
https://dl.acm.org/doi/10.1145/2593882.2593899
Cao HZhang HYan FHuang B(2011)Formal analysis research for information flow of software2011 2nd International Conference on Control, Instrumentation and Automation (ICCIA)10.1109/ICCIAutom.2011.6183958(246-249)Online publication date: Dec-2011
https://doi.org/10.1109/ICCIAutom.2011.6183958
Olender KOsterweil L(2011)Cecil: A Sequencing Constraint Language for Automatic Static Analysis GenerationEngineering of Software10.1007/978-3-642-19823-6_7(115-141)Online publication date: 2011
https://doi.org/10.1007/978-3-642-19823-6_7
Shankar N(2009)Automated deduction for verificationACM Computing Surveys10.1145/1592434.159243741:4(1-56)Online publication date: 9-Oct-2009
https://dl.acm.org/doi/10.1145/1592434.1592437
Osterweil LFosdick L(2006)Dave—a validation error detection and documentation system for fortran programsSoftware: Practice and Experience10.1002/spe.43800604056:4(473-486)Online publication date: 27-Oct-2006
https://doi.org/10.1002/spe.4380060405
Spier MHastings TCutler D(2006)A storage mapping technique for the implementation of protective domainsSoftware: Practice and Experience10.1002/spe.43800403044:3(215-230)Online publication date: 27-Oct-2006
https://doi.org/10.1002/spe.4380040304
Gaines B(2005)Analogy categories, virtual machines, and structured programmingGI — 5. Jahrestagung10.1007/3-540-07410-4_669(691-700)Online publication date: 4-Jun-2005
https://doi.org/10.1007/3-540-07410-4_669
Neumann P(2005)Toward a methodology for designing large systems and verifying their propertiesGl-4.Jahrestagung10.1007/3-540-07141-5_209(52-67)Online publication date: 23-May-2005
https://doi.org/10.1007/3-540-07141-5_209
Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

References

Cited By

Recommendations

Test data as an aid in proving program correctness

Test data as an aid in proving program correctness

Proving Correctness of an Efficient Abstraction for Interrupt Handling

Comments

Information

Published In

Publisher

Publication History

Permissions

Check for updates

Qualifiers

Contributors

Other Metrics

Bibliometrics

Article Metrics

Other Metrics

Citations

Cited By

View options

PDF

eReader

Login options

Full Access

Figures

Other

Share

Share this Publication link

Share on social media

Affiliations