{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T21:43:27Z","timestamp":1725486207776},"publisher-location":"Berlin, Heidelberg","reference-count":33,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540423140"},{"type":"electronic","value":"9783540477648"}],"license":[{"start":{"date-parts":[[2001,1,1]],"date-time":"2001-01-01T00:00:00Z","timestamp":978307200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2001]]},"DOI":"10.1007\/3-540-47764-0_2","type":"book-chapter","created":{"date-parts":[[2007,6,12]],"date-time":"2007-06-12T04:55:55Z","timestamp":1181624155000},"page":"20-39","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Communication and Parallelism Introduction and Elimination in Imperative Concurrent Programs"],"prefix":"10.1007","author":[{"given":"Miquel","family":"Bertran","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Francesc","family":"Babot","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"August","family":"Climent","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Miquel","family":"Nicolau","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2001,7,4]]},"reference":[{"key":"2_CR1","doi-asserted-by":"crossref","unstructured":"R.-J. Back, J. von Wright, Refinement Calculus. A Systematic Introduction. Springer-Verlag 1998.","DOI":"10.1007\/978-1-4612-1674-2"},{"key":"2_CR2","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"58","DOI":"10.1007\/978-3-540-45099-3_4","volume-title":"Static Analysis, Proc. 7th Intl. Symp. SAS 2000","author":"S. Bensalem","year":"2000","unstructured":"S. Bensalem, M. Bozga, J.C. Fernandez, L. Ghirvu, Y. Lakhnech, A Transformational Approach for Generating Non-Linear Invariants. In J. Palsberg (Ed.), Static Analysis, Proc. 7th Intl. Symp. SAS 2000, Santa Barbara, CA, USA, June 29\u2013July 1, 2000. LNCS Vol. 1824, Springer, 2000, pp. 58\u201374."},{"key":"2_CR3","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-63010-4","volume-title":"Transformation-Based Reactive Systems Development","author":"M. Bertran","year":"1997","unstructured":"M. Bertran, F. Alvarez-Cuevas, A. Duran, Communication Extended Abstract Types in the Refinement of Parallel Communicating Processes, in Transformation-Based Reactive Systems Development, LNCS v. 1231, Springer, 1997."},{"key":"2_CR4","doi-asserted-by":"crossref","unstructured":"N.S. Bj\u00f8rner, A. Browne, M. Col\u00f3n, B. Finkbeiner, Z. Manna, H.B. Sipma, and T.E. Uribe. Verifying Temporal Properties of Reactive Systems: A STeP Tutorial. Formal Methods in System Design, 16, 227\u2013270, June 2000.","DOI":"10.1023\/A:1008700623084"},{"key":"2_CR5","unstructured":"N.S. Bj\u00f8rner, A. Browne, E. Chang, M. Col\u00f3n, A. Kapur, Z. Manna, H.B. Sipma, and T.E. Uribe. STeP: The Stanford Temporal Prover, User\u2019s Manual. Technical Report STAN-CS-TR-95-1562, Computer Science Department, Stanford University, November 1995."},{"issue":"2","key":"2_CR6","doi-asserted-by":"crossref","first-page":"145","DOI":"10.1006\/inco.1996.0056","volume":"127","author":"S.D. Brookes","year":"1996","unstructured":"S.D. Brookes. \u2018Full abstraction for a shared variable parallel language\u2019, Information and Computation, 127(2):145\u2013163, June 1996.","journal-title":"Information and Computation"},{"key":"2_CR7","doi-asserted-by":"crossref","unstructured":"M. Broy, \u2018Functional Specification of Time-Sensitive Communicating Systems\u2019, ACM Transactions on Software Engineering and Methodology, 2(1),: 1\u201346, January 1993.","DOI":"10.1145\/151299.151302"},{"key":"2_CR8","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"44","DOI":"10.1007\/3-540-63010-4_4","volume-title":"Transformation-Based Reactive Systems Development","author":"M. Broy","year":"1997","unstructured":"M. Broy, \u2018Refinement of Time\u2019, in M. Bertran and T. Rus (eds.), Transformation-Based Reactive Systems Development, Springer-Verlag, Lecture Notes in Computer Science 1231, 1997, pp. 44\u201363."},{"key":"2_CR9","unstructured":"M. Broy, \u2018A Logical Basis for Component-Based Systems Engineering\u2019, Tech. Report Inst. fr Informatik, Tech. Univ. Munchen, Germany."},{"key":"2_CR10","doi-asserted-by":"crossref","unstructured":"K.M. Chandy and J. Misra, Parallel Program Design, Addison Wesley, 1988.","DOI":"10.1007\/978-1-4613-9668-0_6"},{"key":"2_CR11","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"75","DOI":"10.1007\/978-3-540-45099-3_5","volume-title":"Static Analysis, Proc. 7th Intl. Symp. SAS","author":"W.-N. Chin","year":"2000","unstructured":"Wei-Ngan Chin, Sian-Cheng Khoo, Z. Hu, M. Takeidu, Deriving Parallel Codes via Invariants. In J. Palsberg (Ed.), Static Analysis, Proc. 7th Intl. Symp. SAS 2000, Santa Barbara, CA, USA, June 29\u2013July 1, 2000. LNCS Vol. 1824, Springer, 2000, pp. 75\u201394."},{"key":"2_CR12","unstructured":"E.M. Clarke, O. Grumberg, D.A. Peled, Model Checking, The MIT Press, 1999."},{"key":"2_CR13","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"231","DOI":"10.1007\/3-540-49253-4_18","volume-title":"Algebraic Methodology and Software Technology, AMAST\u201998","author":"J. Dingel","year":"1998","unstructured":"J. Dingel, \u2018A Trace-Based Refinement Calculus for Shared-Variable Parallel Programs\u2019, in A.Martin Haeberer (Ed.) Algebraic Methodology and Software Technology, AMAST\u201998, LNCS 1548, Springer-Verlag, pp. 231\u2013247, 1998."},{"key":"2_CR14","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"239","DOI":"10.1007\/3-540-49213-5_9","volume-title":"Deductive Verification of Modular Systems","author":"B. Finkbeiner","year":"1998","unstructured":"B. Finkbeiner, Z. Manna, H. Sipma, Deductive Verification of Modular Systems. In Compositionality: The Significant Difference, COMPOS\u201997, LNCS v. 1536, pp. 239\u2013275, Springer 1998."},{"key":"2_CR15","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-09724-4","volume-title":"Edinburgh LCF","author":"M. Gordon","year":"1979","unstructured":"M. Gordon, A.J. Milner, Ch. P. Wadsworth, Edinburgh LCF, LNCS v. 78, Springer-Verlag, 1979."},{"key":"2_CR16","doi-asserted-by":"publisher","first-page":"666","DOI":"10.1145\/359576.359585","volume":"21","author":"C.A.R. Hoare","year":"1978","unstructured":"C.A.R. Hoare, \u2018Communicating Sequential Processes\u2019, Communications of ACM, Vol 21, pp 666\u2013677, 1978.","journal-title":"Communications of ACM"},{"key":"2_CR17","volume-title":"Communicating Sequential Processes","author":"C.A.R. Hoare","year":"1985","unstructured":"C.A.R. Hoare, Communicating Sequential Processes, Prentice-Hall, Englewood Cliffs, N.J., 1985."},{"key":"2_CR18","unstructured":"Gerald Holtzmann, Design and Validation of Computer Protocols, Prentice Hall, 1991."},{"key":"2_CR19","doi-asserted-by":"publisher","first-page":"801","DOI":"10.1007\/BF01213604","volume":"6A","author":"J. Hooman","year":"1994","unstructured":"J. Hooman, \u2018Extending Hoare Logic to Real-Time\u2019, Formal Aspects of Computing, 6A: 801\u2013825, BCS, 1994.","journal-title":"Formal Aspects of Computing"},{"key":"2_CR20","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"273","DOI":"10.1007\/3-540-58043-3_22","volume-title":"REX Symposium A Decade of Concurrency","author":"Y. Kesten","year":"1994","unstructured":"Y. Kesten, Z. Manna, A. Pnueli, \u2018Temporal Verification of Simulation and Refinement\u2019, In REX Symposium A Decade of Concurrency, Lecture Notes in Computer Science 803, pp. 273\u2013346, Springer-Verlag, 1994."},{"key":"2_CR21","doi-asserted-by":"crossref","unstructured":"L. Lamport, \u2018The Temporal Logic of Actions\u2019, ACM Trans. Progr. Lang. and Sys., 16(3):872\u2013923.","DOI":"10.1145\/177492.177726"},{"key":"2_CR22","unstructured":"B. Mahony, \u2018Using the Refinement Calculus for Dataflow Processes\u2019. Tech. Report 94-32, Soft. Verification Research Centre, University of Queensland, October 94."},{"key":"2_CR23","doi-asserted-by":"crossref","unstructured":"Z. Manna, A. Pnueli, The Temporal Logic of Reactive and Concurrent Systems. Specification. Springer-Verlag, 1991.","DOI":"10.1007\/978-1-4612-0931-7"},{"key":"2_CR24","doi-asserted-by":"crossref","unstructured":"Z. Manna, A. Pnueli, Temporal Verification of Reactive Systems. Safety. Springer-Verlag, 1995.","DOI":"10.1007\/978-1-4612-4222-2"},{"key":"2_CR25","doi-asserted-by":"crossref","unstructured":"K.L. McMillan, and D.L. Dill, Symbolic Model Checking: An Approach to the State Explosion Problem, Kluwer Academic, 1993.","DOI":"10.1007\/978-1-4615-3190-6_3"},{"key":"2_CR26","doi-asserted-by":"crossref","unstructured":"R. Milner, A Calculus of Communicating Systems, Springer-Verlag, 1980.","DOI":"10.1007\/3-540-10235-3"},{"key":"2_CR27","unstructured":"R. Milner, Communication and Concurrency, Prentice-Hall 1989."},{"key":"2_CR28","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"330","DOI":"10.1007\/3-540-48294-6_22","volume-title":"Static Analysis, Proc. 6th Intl. Symp. SAS\u201999","author":"M. Muller-Olm","year":"1999","unstructured":"M. Muller-Olm, D.A. Schmit, B. Steffen, Model Checking: A Tutorial Introduction. In A Cortesi, G File (Eds.), Static Analysis, Proc. 6th Intl. Symp. SAS\u201999, Venice, Italy, September 22\u201324, 1999. LNCS, Vol 1694, Springer, 1999, pp. 330\u2013354."},{"key":"2_CR29","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"75","DOI":"10.1007\/978-3-540-45099-3_5","volume-title":"Static Analysis, Proc. 7th Intl. Symp. SAS","author":"W.-N. Chin","year":"2000","unstructured":"Wei-Ngan Chin, Sian-Cheng Khoo, Z. Hu, M. Takeidu, Deriving Parallel Codes via Invariants. In J. Palsberg (Ed.), Static Analysis, Proc. 7th Intl. Symp. SAS 2000, Santa Barbara, CA, USA, June 29\u2013July 1, 2000. LNCS Vol. 1824, Springer, 2000, pp. 75\u201394."},{"key":"2_CR30","volume-title":"Digital Signal Processing","author":"A.V. Oppenheim","year":"1975","unstructured":"A.V. Oppenheim, R.W. Shafer, Digital Signal Processing, Prentice Hall, N.J., 1975."},{"key":"2_CR31","volume-title":"Signal Analysis","author":"A. Papoulis","year":"1977","unstructured":"A. Papoulis, Signal Analysis, McGraw-Hill, N.Y., 1977."},{"key":"2_CR32","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"22","DOI":"10.1007\/978-3-540-45099-3_2","volume-title":"Static Analysis, Proc. 7th Intl. Symp. SAS","author":"A. Podelski","year":"2000","unstructured":"A. Podelski, Model Checking as Constraint Solving. In J. Palsberg (Ed.), Static Analysis, Proc. 7th Intl. Symp. SAS 2000, Santa Barbara, CA, USA, June 29\u2013July 1, 2000. LNCS Vol. 1824, Springer, 2000, pp. 22\u201337."},{"key":"2_CR33","volume-title":"Theory and Application of Digital Signal processing","author":"L.R. Rabiner","year":"1975","unstructured":"L.R. Rabiner, B. Gold, Theory and Application of Digital Signal processing, Prentice Hall, N.J., 1975."}],"container-title":["Lecture Notes in Computer Science","Static Analysis"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-47764-0_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,19]],"date-time":"2019-05-19T13:32:08Z","timestamp":1558272728000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-47764-0_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001]]},"ISBN":["9783540423140","9783540477648"],"references-count":33,"URL":"https:\/\/doi.org\/10.1007\/3-540-47764-0_2","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2001]]},"assertion":[{"value":"4 July 2001","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}