{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,9]],"date-time":"2026-05-09T03:39:51Z","timestamp":1778297991787,"version":"3.51.4"},"publisher-location":"Berlin, Heidelberg","reference-count":18,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540100034","type":"print"},{"value":"9783540393467","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1980]]},"DOI":"10.1007\/3-540-10003-2_69","type":"book-chapter","created":{"date-parts":[[2012,2,25]],"date-time":"2012-02-25T11:59:22Z","timestamp":1330171162000},"page":"169-181","source":"Crossref","is-referenced-by-count":157,"title":["Characterizing correctness properties of parallel programs using fixpoints"],"prefix":"10.1007","author":[{"given":"E. Allen","family":"Emerson","sequence":"first","affiliation":[]},{"given":"Edmund M.","family":"Clarke","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,5,24]]},"reference":[{"issue":"1","key":"16_CR1","doi-asserted-by":"crossref","first-page":"339","DOI":"10.1109\/TSE.1975.6312858","volume":"SE-1","author":"S. K. Basu","year":"1975","unstructured":"Basu, S.K. and Yeh, R.T., Strong Verification of Programs. IEEE Trans. on Software Engineering, v. SE-1. no. 1, pp.339\u2013354, September 1975.","journal-title":"IEEE Trans. on Software Engineering"},{"key":"16_CR2","doi-asserted-by":"crossref","unstructured":"Chandra, A. K., Computable Nondeterministic Functions. 19th Annual Symp. on Foundations of Computer Science, 1978.","DOI":"10.1109\/SFCS.1978.10"},{"key":"16_CR3","doi-asserted-by":"crossref","unstructured":"Clarke, E. M., Program Invariants as Fixpoints. 18th Annual Symp. on Foundations of Computer Science, 1977.","DOI":"10.1109\/SFCS.1977.25"},{"key":"16_CR4","doi-asserted-by":"crossref","unstructured":"Clarke, E. M., Synthesis of Resource Invariants for Concurrent Programs, 6th POPL Conference, January, 1979.","DOI":"10.1145\/567752.567772"},{"key":"16_CR5","volume-title":"Int. Symp. on Programming","author":"P. Cousot","year":"1976","unstructured":"Cousot, P. and Cousot R., Static Determination of Dynamic Properties of Programs. Proc. 2nd Int. Symp. on Programming, (B. Robinet, ed.), Dunod, Paris, April 1976.","edition":"Proc. 2nd"},{"key":"16_CR6","volume-title":"Recursive Programs as Predicate Transformers","author":"J. W. Bakker de","year":"1977","unstructured":"de Bakker, J. W., Recursive Programs as Predicate Transformers. Mathematical Centre, Amsterdam, 1977."},{"key":"16_CR7","volume-title":"Semantics of Infinite Processes Using Generalized Trees","author":"J. W. Bakker de","year":"1977","unstructured":"de Bakker. J. W., Semantics of Infinite Processes Using Generalized Trees. Mathematical Centre, Amsterdam, 1977."},{"key":"16_CR8","unstructured":"Dijkstra, E. W., A Discipline of Programming, Prentice-Hall, 1976."},{"key":"16_CR9","doi-asserted-by":"crossref","unstructured":"Flon, L. and Suzuki, N., Consistent and Complete Proof Rules for the Total Correctness of Parallel Programs. 19th Annual Symp. on Foundations of Computer Science, 1978.","DOI":"10.1109\/SFCS.1978.11"},{"key":"16_CR10","doi-asserted-by":"crossref","unstructured":"Flon, L. and Suzuki, N., The Total Correctness of Parallel Programs. SIAM J. Comp., to appear","DOI":"10.1137\/0210016"},{"key":"16_CR11","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-662-12898-5","volume-title":"Recursion-Theoretic Hierarchies","author":"P. G. Hinman","year":"1978","unstructured":"Hinman, P. G., Recursion-Theoretic Hierarchies, Springer-Verlag, Berlin, 1978."},{"key":"16_CR12","doi-asserted-by":"crossref","unstructured":"Hoare, C. A. R., An Axiomatic Approach to Computer Programming CACM, v.10. no 12., pp.322\u2013329, October 1969.","DOI":"10.1145\/363235.363259"},{"key":"16_CR13","doi-asserted-by":"crossref","unstructured":"Meyer, A. R. and Winklmann, K., On the Expressive Power of Dynamic Logic. Proceedings of the 11th Annual ACM Symp. on Theory of Computing, 1979.","DOI":"10.1145\/800135.804410"},{"key":"16_CR14","unstructured":"Park, D., Fixpoint Induction and Proofs of Program Properties, in Machine Intelligence 5, (D. Mitchie, ed.) Edinburgh University Press, 1970."},{"key":"16_CR15","doi-asserted-by":"crossref","unstructured":"Reif, J. H., Data Flow Analysis of Communicating Processes. 6th POPL Conference, January 1979.","DOI":"10.1145\/567752.567777"},{"key":"16_CR16","volume-title":"Theory of Recursive Functions and Effective Computability","author":"H. R. Rogers","year":"1967","unstructured":"Rogers, H. R., Theory of Recursive Functions and Effective Computability, McGraw-Hill, New York, 1967."},{"key":"16_CR17","unstructured":"Sintzoff, M. and Van Lamsweerde, A., Formal Derivation of Strongly Correct Parallel Programs, M. B. L. E. Research Lab., Brussels, Report R338, October 1976."},{"key":"16_CR18","doi-asserted-by":"crossref","first-page":"285","DOI":"10.2140\/pjm.1955.5.285","volume":"5","author":"A. Tarski","year":"1955","unstructured":"Tarski, A., A Lattice-Theoretical Fixpoint Theorem and Its Applications. Pacific J. Math., 5, pp.285\u2013309 (1955).","journal-title":"Pacific J. Math."}],"container-title":["Lecture Notes in Computer Science","Automata, Languages and Programming"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-10003-2_69.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T15:02:18Z","timestamp":1605625338000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-10003-2_69"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1980]]},"ISBN":["9783540100034","9783540393467"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/3-540-10003-2_69","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[1980]]}}}