{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,6]],"date-time":"2025-10-06T09:07:30Z","timestamp":1759741650485},"reference-count":26,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[1979,12,1]],"date-time":"1979-12-01T00:00:00Z","timestamp":312854400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Computing"],"published-print":{"date-parts":[[1979,12]]},"DOI":"10.1007\/bf02248730","type":"journal-article","created":{"date-parts":[[2005,11,15]],"date-time":"2005-11-15T04:24:19Z","timestamp":1132028659000},"page":"273-294","source":"Crossref","is-referenced-by-count":20,"title":["Program invariants as fixedpoints"],"prefix":"10.1007","volume":"21","author":[{"given":"E. M.","family":"Clarke","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"BF02248730_CR1","doi-asserted-by":"crossref","unstructured":"Cherniavsky, J., Kamin, S.: A complete and consistent Hoare axiomatics for a simple programming language. Proceedings of the 4th POPL, 1977.","DOI":"10.1145\/512950.512951"},{"key":"BF02248730_CR2","doi-asserted-by":"crossref","unstructured":"Clarke, E. M.: Programming language constructs for which it is impossible to obtain good Hoare-like axiom systems. Proceedings of the 4th POPL, 1977.","DOI":"10.1145\/512950.512952"},{"key":"BF02248730_CR3","unstructured":"Cook, S. A.: Axiomatic and interpretative semantics for an algol fragment. Technical Report 79, Department of Computer Science, University of Toronto, 1975 (to be published in SCICOMP)."},{"key":"BF02248730_CR4","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation: A unified lattice model for static analysis of Programs by construction or approximation of Fixpoints. Proceedings of the 4th POPL, 1977.","DOI":"10.1145\/512950.512973"},{"key":"BF02248730_CR5","unstructured":"deBakker, J. W., Meertens, L. G. L. Th.: On the completeness of the induction assertion method. Mathematical Centre, December 1973."},{"key":"BF02248730_CR6","unstructured":"de Bakker, J. W.: Fixed point semantics and Dijkstra's fundamental invariance theorem. Mathematical Centre, January 1975."},{"key":"BF02248730_CR7","doi-asserted-by":"crossref","unstructured":"deBakker, J. W.: Flow of control in the proof theory of structured programming. Mathematical Centre, 1975.","DOI":"10.1109\/SFCS.1975.15"},{"key":"BF02248730_CR8","unstructured":"Dijkstra, E. E.: A simple axiomatic basis for programming language constructs. Lecture notes from the International Summer School on Structured Programming and Programmed Structures, Munich, Germany, 1973."},{"key":"BF02248730_CR9","unstructured":"Donahue, J.: Mathematical semantics as a complementary definition for axiomatically defined programming language constructs. Technical Report CSRG-45, Computer Systems Research Group, University of Toronto, December 1974."},{"key":"BF02248730_CR10","doi-asserted-by":"crossref","unstructured":"Floyd, R. W.: Assigning meaning to programs. In: Mathematical Aspects of Computer Science Proc. Symposia in Applied Mathematics (Schwartz, J. T., ed.), Vol. 19, pp. 19\u201332. Amer. Math. Soc. 1967.","DOI":"10.1090\/psapm\/019\/0235771"},{"key":"BF02248730_CR11","doi-asserted-by":"crossref","unstructured":"Fokkinga, M. C.: Inductive assertion patterns for recursive procedures. Techn. University Delft Report, 1973.","DOI":"10.1007\/3-540-06859-7_136"},{"key":"BF02248730_CR12","doi-asserted-by":"crossref","unstructured":"Gerhart, S. L.: Proof theory of partial correctness verification systems. SIAM J. Comput.5 (1976).","DOI":"10.1137\/0205030"},{"key":"BF02248730_CR13","unstructured":"Gorelick, G.: A complete axiomatic system for proving assertions about recursive and nonrecursive programs. Technical Report No. 75, Department of Computer Science, University of Toronto, January 1975."},{"key":"BF02248730_CR14","first-page":"322","volume":"12","author":"C. A. R. Hoare","year":"1969","unstructured":"Hoare, C. A. R.: An axiomatic approach to computer programming. CACM12, 322\u2013329 (1969).","journal-title":"CACM"},{"key":"BF02248730_CR15","series-title":"Symposium on Semantics of Algorithmic Languages","first-page":"102","volume-title":"Procedures and parameters: An axiomatic approach","author":"C. A. R. Hoare","year":"1971","unstructured":"Hoare, C. A. R.: Procedures and parameters: An axiomatic approach. Symposium on Semantics of Algorithmic Languages (Engeler, E., ed.), pp. 102\u2013116. Berlin-Heidelberg-New York: Springer 1971."},{"key":"BF02248730_CR16","first-page":"135","volume":"3","author":"C. A. R. Hoare","year":"1974","unstructured":"Hoare, C. A. R., Lauer, P. E.: Consistent and complementary formal theories of the semantics of programming languages. Acta Informatica3, 135\u2013154 (1974).","journal-title":"Acta Informatica"},{"key":"BF02248730_CR17","doi-asserted-by":"crossref","unstructured":"Lipton, R.: A necessary and sufficient condition for the existence of Hoare Logics. 18 Annual Symposium on Foundations of Computer Science, 1977.","DOI":"10.1109\/SFCS.1977.1"},{"key":"BF02248730_CR18","doi-asserted-by":"crossref","first-page":"555","DOI":"10.1145\/321592.321606","volume":"17","author":"Z. Manna","year":"1970","unstructured":"Manna, Z., Pnueli, A.: Formalization of properties of functional programs. JACM17, 555\u2013569 (1970).","journal-title":"JACM"},{"key":"BF02248730_CR19","unstructured":"McGowan, C., Misra, J.: A mathematical basis for Dijkstra-Hoare semantics. Technical Report No. 73-73, Center for Computer and Information Sciences, Brown University, November 1973."},{"key":"BF02248730_CR20","first-page":"59","volume":"5","author":"D. Park","year":"1970","unstructured":"Park, D.: Fixpoint induction and proofs of program properties. Machine Intelligence5, 59\u201378 (1970).","journal-title":"Machine Intelligence"},{"key":"BF02248730_CR21","doi-asserted-by":"crossref","unstructured":"Owicki, S.: A consistent and complete deductive system for the verification of parallel programs. 8th Annual Symposium on Theory of Computing, 1976.","DOI":"10.1145\/800113.803634"},{"key":"BF02248730_CR22","unstructured":"Scott, D.: Outline of a mathematical theory of computation. Proceeding of Fourth Annual Princeton Conference on Information Science and Systems. Princeton, pp. 169\u2013176, 1970."},{"key":"BF02248730_CR23","series-title":"Springer Notes in Mathematics","doi-asserted-by":"crossref","first-page":"311","DOI":"10.1007\/BFb0059703","volume-title":"The lattice of flow diagrams. Semantics of Algorithmic Languages","author":"D. Scott","year":"1971","unstructured":"Scott D.: The lattice of flow diagrams. Semantics of Algorithmic Languages (Springer Notes in Mathematics, Vol. 188), (Engeler, E., ed.), pp. 311\u2013366. Berlin-Heidelberg-New York: Springer 1971."},{"key":"BF02248730_CR24","doi-asserted-by":"crossref","unstructured":"Suzuki, N., Ishihata, K.: Implementation of an array bound checker. Proceedings of the 4th POPL, 1977.","DOI":"10.1145\/512950.512963"},{"key":"BF02248730_CR25","doi-asserted-by":"crossref","unstructured":"Wand, M.: A new incompleteness result for Hoare's system. 8th Annual Symposium on Theory of Computing, 1976.","DOI":"10.1145\/800113.803635"},{"issue":"4","key":"BF02248730_CR26","first-page":"244","volume":"2","author":"R. T. Yeh","year":"1976","unstructured":"Yeh, R. T., Reynolds, C.: Induction as the basis for program verification. IEEE Transactions on Software Engineering, SE-2(4), 244\u2013252 (1976).","journal-title":"IEEE Transactions on Software Engineering"}],"container-title":["Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF02248730.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/BF02248730\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF02248730","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,10]],"date-time":"2020-04-10T22:22:19Z","timestamp":1586557339000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BF02248730"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1979,12]]},"references-count":26,"journal-issue":{"issue":"4","published-print":{"date-parts":[[1979,12]]}},"alternative-id":["BF02248730"],"URL":"https:\/\/doi.org\/10.1007\/bf02248730","relation":{},"ISSN":["0010-485X","1436-5057"],"issn-type":[{"value":"0010-485X","type":"print"},{"value":"1436-5057","type":"electronic"}],"subject":[],"published":{"date-parts":[[1979,12]]}}}