article

Free access

Complexity of Synthesizing Inductive Assertions

Author:

Ben WegbreitAuthors Info & Claims

Journal of the ACM (JACM), Volume 24, Issue 3

Pages 504 - 512

https://doi.org/10.1145/322017.322029

Published: 01 July 1977 Publication History

PDF eReader

References

[1]

BASU, S K, AND MISRA, J Proving loop programs 1EEE Trans Software Eng SE-1, 1 (March 1975), 76-86

Google Scholar

[2]

CHANG, C L A test-oriented method for generating inductive asseruons m program verification IBM Res Lab, San Jose, Cahf

Google Scholar

[3]

CHANG, C L, LEE, R C T, ANt~ SLAGLE, J R A direct method for verifying programs Heunstacs Lab, NIH, Bethesda, Md,

Google Scholar

[4]

Coo~, S The complexity of theorem-proving procedures Third Annual ACM Symp on Theory of Computmg, ACM, NewYork, 1971,pp 15t-158

Crossref

Google Scholar

[5]

COOPER, D C Programs for mechanical program verification In Machine Intelhgence 6, B Meltzer and D Mlchae, Eds . Ameracan Elsevaer, New York, 1971

Google Scholar

[6]

ELSPAS. B The semiautomatic generation of inductive assertaons for provmg program correctness SRI Prol 2686, Stanford Research lnst, Menlo Park, Cahf, July 1974

Google Scholar

[7]

ELSPAS, B, GREEN, M W, L~vrrT, K N, ANO WALDINGER, R J Research m interacttve programproving techntques SRI Prol 8398. Stanford Research IrLst . Menlo Park, Calif., May 1972

Google Scholar

[8]

FLoyD, R Assigning meanings to programs Proc Syrup in Applied Math, Vol 19, J.T Schwartz, Ed, AMS, Provzdence. R I, 1967 pp 19-32

Google Scholar

[9]

GERMAN, S, ANt) WEGBREIT, B A synthestzer of mductwe asserttons IEEE Trans. Software Eng SE-1, I (March 1975), 68-75

Google Scholar

[10]

GREIF, 1, AND WALDINGER,.R A more mechanical heunstac approach to program verlficataon Internat Symp on Programming, Paras, April 1974, pp 83-90

Crossref

Google Scholar

[11]

JohNson, D Near-optimal bin packing algonthms Ph D Th, MAC TR-109, M.I.T, Cambridge. Mass, June 1973

Google Scholar

[12]

KARP, R M Reduobfllty among comblnatorml problems In Complemtv of Computer Computations, R Miller and J Thatcher, Eds, Plenum Press. New York, 1972

Google Scholar

[13]

KATZ S M, AND MANNA, Z A heunstac approach to program venficauon Proc. 3rd lnternat Joint Conf on ArtJf Intel, Aug 1973, pp 500-512

Google Scholar

[14]

KATZ, S, AND MANNA, Z Logical analys~s of programs Dept of Apphed Math, Wozmann Inst of Science, Rehovot, Israel, July 1974

Google Scholar

[15]

MAN~A, Z The correctness of programs J Comptr Syst Scl 3 (1969), 119-127

Google Scholar

[16]

MOORE, JS. Introducmg PROG into the pure L~sp theorem prover. CSL-74-3~ Xerox Palo Alto Res Ctr., Palo Alto, Calif., Dec. 1974

Google Scholar

[17]

Moi~Ico~r, M. Semiautomatic synthes~s of induct~ve predtcates ATP-16, Depts. Math. and Comptr. Sci, U of Texas, Austin, Tex., June 1974.

Google Scholar

[18]

NOONAN, R E. A simple heuristic for completing loop predicates Dept Comptr Sc~, U. of Maryland, College Park, Md., 1974

Google Scholar

[19]

WEGBREIT, B. The synthesis of loop predicates Comm ACM 17, 2 (Feb. 1974), 102-112

Crossref

Google Scholar

Cited By

View all

Fribourg L(1992)Mixing list recursion and arithmetic[1992] Proceedings of the Seventh Annual IEEE Symposium on Logic in Computer Science10.1109/LICS.1992.185553(419-429)Online publication date: 1992
https://doi.org/10.1109/LICS.1992.185553
Dunlop DBasili V(1985)Generalizing specifications for uniformly implemented loopsACM Transactions on Programming Languages and Systems10.1145/2363.27087:1(137-158)Online publication date: 2-Jan-1985
https://dl.acm.org/doi/10.1145/2363.2708
Dunlop DBasili V(1984)A heuristic for deriving loop functionsIEEE Transactions on Software Engineering10.1109/TSE.1984.501023610:3(275-285)Online publication date: 26-May-1984
https://dl.acm.org/doi/10.1109/TSE.1984.5010236
Show More Cited By

Index Terms

Complexity of Synthesizing Inductive Assertions
1. Software and its engineering
  1. Software organization and properties
    1. Software functional properties
      1. Correctness
2. Theory of computation
  1. Logic
    1. Proof theory
  2. Semantics and reasoning
    1. Program reasoning
      1. Program verification

Recommendations

Linear Complexity Assertions for Sorting

Correctness of the execution of sorting programs can be checked by two assertions: the order assertion and the permutation assertion. The order assertion checks if the sorted data is in ascending or descending order. The permutation assertion checks if ...
A synthesizer of inductive assertions

Most current methods for mechanical program verification require a complete inductive assertion on each loop. As this is tedious and error prone, producing a program with complete, correct assertions is moderately difficult. This paper describes a ...
Parameterized Verification with Automatically Computed Inductive Assertions
CAV '01: Proceedings of the 13th International Conference on Computer Aided Verification

The paper presents a method, called the method of verification by invisible invariants, for the automatic verification of a large class of parameterized systems. The method is based on the automatic calculation of candidate inductive assertions and ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

Journal of the ACM Volume 24, Issue 3

July 1977

175 pages

ISSN:0004-5411

EISSN:1557-735X

DOI:10.1145/322017

Issue’s Table of Contents

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 01 July 1977

Published in JACM Volume 24, Issue 3

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

9
Total Citations
View Citations
394
Total Downloads

Downloads (Last 12 months)57
Downloads (Last 6 weeks)11

Reflects downloads up to 23 Jan 2025

Other Metrics

View Author Metrics

Citations

Cited By

View all

Fribourg L(1992)Mixing list recursion and arithmetic[1992] Proceedings of the Seventh Annual IEEE Symposium on Logic in Computer Science10.1109/LICS.1992.185553(419-429)Online publication date: 1992
https://doi.org/10.1109/LICS.1992.185553
Dunlop DBasili V(1985)Generalizing specifications for uniformly implemented loopsACM Transactions on Programming Languages and Systems10.1145/2363.27087:1(137-158)Online publication date: 2-Jan-1985
https://dl.acm.org/doi/10.1145/2363.2708
Dunlop DBasili V(1984)A heuristic for deriving loop functionsIEEE Transactions on Software Engineering10.1109/TSE.1984.501023610:3(275-285)Online publication date: 26-May-1984
https://dl.acm.org/doi/10.1109/TSE.1984.5010236
Nepomnyashchii V(1984)Practical methods of program verificationCybernetics10.1007/BF0106917420:2(193-203)Online publication date: 1984
https://doi.org/10.1007/BF01069174
Dunlop DBasili V(1982)A Comparative Analysis of Functional CorrectnessACM Computing Surveys10.1145/356876.35688114:2(229-244)Online publication date: 1-Jun-1982
https://dl.acm.org/doi/10.1145/356876.356881
Laski J(1980)A hierarchical approach to program testingACM SIGPLAN Notices10.1145/954127.95413515:1(77-85)Online publication date: 1-Jan-1980
https://dl.acm.org/doi/10.1145/954127.954135
Basu S(1980)A Note on Synthesis of Inductive AssertionsIEEE Transactions on Software Engineering10.1109/TSE.1980.2304606:1(32-39)Online publication date: 1-Jan-1980
https://dl.acm.org/doi/10.1109/TSE.1980.230460
Jones NMuchnick S(1980)Complexity of flow analysis, inductive assertion synthesis and a language due to DijkstraProceedings of the 21st Annual Symposium on Foundations of Computer Science10.1109/SFCS.1980.16(185-190)Online publication date: 13-Oct-1980
https://dl.acm.org/doi/10.1109/SFCS.1980.16
Bate RLigler G(1978)An approach to software testing: methodology and toolsThe IEEE Computer Society's Second International Computer Software and Applications Conference, 1978. COMPSAC '78.10.1109/CMPSAC.1978.810468(476-480)Online publication date: 1978
https://doi.org/10.1109/CMPSAC.1978.810468

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

Index Terms

Recommendations

Linear Complexity Assertions for Sorting

A synthesizer of inductive assertions

Parameterized Verification with Automatically Computed Inductive Assertions

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