{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T21:08:59Z","timestamp":1725484139249},"publisher-location":"Berlin, Heidelberg","reference-count":30,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540439288"},{"type":"electronic","value":"9783540456148"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-45614-7_10","type":"book-chapter","created":{"date-parts":[[2007,5,17]],"date-time":"2007-05-17T04:45:28Z","timestamp":1179377128000},"page":"163-183","source":"Crossref","is-referenced-by-count":5,"title":["Mechanical Abstraction of CSPZ Processes"],"prefix":"10.1007","author":[{"given":"Alexandre","family":"Mota","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Paulo","family":"Borba","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Augusto","family":"Sampaio","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2002,7,9]]},"reference":[{"key":"10_CR1","unstructured":"A. Mota. Model checking CSP Z: Techniques to Overcome State Explosion. PhD thesis, Universidade Federal de Pernambuco, 2002."},{"key":"10_CR2","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"205","DOI":"10.1007\/BFb0053592","volume-title":"Proceedings of the European Joint Conference on Theory and Practice of Software","author":"A. Mota","year":"1998","unstructured":"A. Mota and A. Sampaio. Mo del-Checking CSP-Z. In Proceedings of the European Joint Conference on Theory and Practice of Software, volume 1382 of LNCS, pages 205\u2013220. Springer-Verlag, 1998."},{"key":"10_CR3","doi-asserted-by":"publisher","first-page":"59","DOI":"10.1016\/S0167-6423(00)00023-X","volume":"40","author":"A. Mota","year":"2001","unstructured":"A. Mota and A. Sampaio. Model-Checking CSP-Z: Strategy, Tool Support and Industrial Application. Science of Computer Programming, 40:59\u201396, 2001.","journal-title":"Science of Computer Programming"},{"key":"10_CR4","unstructured":"A.W. Roscoe. The Theory and Practice of Concurrency. Prentice Hall, 1998."},{"key":"10_CR5","series-title":"Lect Notes Comput Sci","first-page":"01","volume-title":"On the Expressiveness of Real and Integer Arithmetic Automata (Extended Abstract)","author":"B. Boigelot","year":"1999","unstructured":"B. Boigelot, S. Rassart, and P. Wolper. On the Expressiveness of Real and Integer Arithmetic Automata (Extended Abstract). LNCS, 1443:01\u201352, 1999."},{"key":"10_CR6","doi-asserted-by":"crossref","unstructured":"C.A.R. Hoare. Communicating Sequential Processes. Prentice-Hall, 1985.","DOI":"10.1007\/978-3-642-82921-5_4"},{"key":"10_CR7","unstructured":"C. Fischer. Combining CSP and Z. Technical report, Univ. Oldenburg, 1996."},{"key":"10_CR8","unstructured":"C. Fischer. Combination and Implementation of Processes and Data: from CSP-OZ to Java. PhD thesis, Fachbereich Informatik Universit\u00e4t Oldenburg, 2000."},{"key":"10_CR9","first-page":"11","volume-title":"Formal Methods in System Design","author":"C. Loiseaux","year":"1995","unstructured":"C. Loiseaux, S. Graf, J. Sifakis, A. Bouajjani, and S. Bensalem. Property Preserving Abstractions for the Verification of Concurrent Systems. In Formal Methods in System Design, volume 6, pages 11\u201344. Kluwer Academic Publishers, Boston, 1995."},{"key":"10_CR10","unstructured":"E.M. Clarke, O. Grumberg, and D.A. Peled. Model Checking. The MIT Press, 1999."},{"key":"10_CR11","unstructured":"J.A.C.F. Neriet al. SACI-1: A cost-effective microssatellite bus for multiple mission payloads. Technical report, Instituto Nacional de Pesquisas Espaciais-INPE, 1995."},{"key":"10_CR12","unstructured":"M. Goldsmith et al. FDR: User Manual and Tutorial, version 2.77. Formal Systems (Europe) Ltd, August 2001."},{"key":"10_CR13","series-title":"Lect Notes Comput Sci","volume-title":"FM\u201999 World Congress on Formal Methods","author":"H. Wehrheim","year":"1999","unstructured":"H. Wehrheim. Data Abstraction for CSP-OZ. In J. Woodcock and J. Wing, editors, FM\u201999 World Congress on Formal Methods. LNCS 1709, Springer, 1999."},{"key":"10_CR14","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1007\/s001650070026","volume":"12","author":"H. Wehrheim","year":"2000","unstructured":"H. Wehrheim. Data Abstraction Techniques in the Validation of CSP-OZ Sp. In Formal Aspects of Computing, volume 12, pages 147\u2013164, 2000.","journal-title":"Formal Aspects of Computing"},{"key":"10_CR15","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"20","DOI":"10.1007\/BFb0054162","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"K. Laster","year":"1998","unstructured":"K. Laster and O. Grumberg. Modular model checking of software. In Tools and Algorithms for the Construction and Analysis of Systems, number 1382 in LNCS, pages 20\u201335, 1998."},{"key":"10_CR16","doi-asserted-by":"crossref","unstructured":"K. Stahl, K. Baukus, Y. Lakhneich, and M. Steffen. Divide, Abstract, and Model Check. SPIN, pages 57\u201376, 1999.","DOI":"10.1007\/3-540-48234-2_5"},{"key":"10_CR17","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"36","DOI":"10.1007\/BFb0054163","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"M. Huhn","year":"1998","unstructured":"M. Huhn, P. Niebert, and F. Wallner. Verification based on local states. In Tools and Algorithms for the Construction and Analysis of Systems, number 1382 in LNCS, pages 36\u201351, 1998."},{"issue":"4","key":"10_CR18","doi-asserted-by":"publisher","first-page":"203","DOI":"10.1109\/32.588534","volume":"23","author":"M. Kaufmann","year":"1997","unstructured":"M. Kaufmann and J. Moore. An Industrial Strength Theorem Prover for a Logic Based on Common Lisp. IEEE Trans. on Software Engineering, 23(4):203\u2013213, 1997.","journal-title":"IEEE Trans. on Software Engineering"},{"key":"10_CR19","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0027284","volume-title":"ZUM\u201997: The Z Formal Specification Notation","author":"M. Saaltink","year":"1997","unstructured":"M. Saaltink. The Z-Eves System. In ZUM\u201997: The Z Formal Specification Notation. LNCS 1212, Springer, 1997."},{"key":"10_CR20","unstructured":"M. Spivey. The Z Notation: A Reference Manual. Prentice-Hall International, 2nd edition, 1992."},{"key":"10_CR21","first-page":"269","volume-title":"Conference Record of the 6th ACM Symp. on Principles of Programming Languages (POPL\u201979)","author":"P. Cousot","year":"1979","unstructured":"P. Cousot and R. Cousot. Systematic design of program analysis frameworks. In Conference Record of the 6th ACM Symp. on Principles of Programming Languages (POPL\u201979), pages 269\u2013282. ACM Press, New York, 1979."},{"issue":"4","key":"10_CR22","doi-asserted-by":"publisher","first-page":"511","DOI":"10.1093\/logcom\/2.4.511","volume":"2","author":"P. Cousot","year":"1992","unstructured":"P. Cousot and R. Cousot. Abstract interpretation frameworks. J. Logic. and Comp., 2(4):511\u2013547, 1992.","journal-title":"J. Logic. and Comp."},{"key":"10_CR23","doi-asserted-by":"crossref","unstructured":"P. Wolper. Expressing interesting properties of programs in propositional temporal logic (extended abstract). In Proc. 13th ACM Symposium on Principles of Programming Languages, pages 184\u2013193, 1986.","DOI":"10.1145\/512644.512661"},{"key":"10_CR24","first-page":"417","volume-title":"CONCUR\u201994","author":"R. Cleaveland","year":"1994","unstructured":"R. Cleaveland and J. Riely. Testing-based abstractions for value-passing systems. In J. Parrow B. Jonsson, editor, CONCUR\u201994, volume 836, pages 417\u2013432. Springer-Verlag Berlin, 1994."},{"issue":"2","key":"10_CR25","doi-asserted-by":"publisher","first-page":"361","DOI":"10.1145\/333979.333989","volume":"47","author":"R. Giacobazzi","year":"2000","unstructured":"R. Giacobazzi and F. Ranzato. Making abstract interpretations complete. Journal of the ACM, 47(2):361\u2013416, 2000.","journal-title":"Journal of the ACM"},{"key":"10_CR26","unstructured":"R. Lazi\u0107. A semantic study of data-independence with applications to the mechanical verification of concurrent systems. PhD thesis, Oxford University, 1999."},{"key":"10_CR27","unstructured":"S.A. Cook and D.G. Mitchell. Satisfiability Problem: Theory and Applications. In Discrete Mathematics and Theoretical Computer Science. AMS, 1997."},{"key":"10_CR28","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"896","DOI":"10.1007\/3-540-48119-2_49","volume-title":"FM\u201999-Formal Methods","author":"S. Liu","year":"1999","unstructured":"S. Liu. Verifying Consistency and Validity of Formal Specifications by Testing. In FM\u201999-Formal Methods, pages 896\u2013914. LNCS 1708, 1999."},{"key":"10_CR29","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"411","DOI":"10.1007\/3-540-61474-5_91","volume-title":"Computer-Aided Verification, CAV\u201996","author":"S. Owre","year":"1996","unstructured":"S. Owre, S. Rajan, J.M. Rushby, N. Shankar, and M.K. Srivas. PVS: Combining Specification, Proof Checking, and Model Checking. In Rajeev Alur and Thomas A. Henzinger, editors, Computer-Aided Verification, CAV\u201996, volume 1102 of LNCS, pages 411\u2013414, New Brunswick, NJ, July\/August 1996. Springer-Verlag."},{"key":"10_CR30","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1007\/3-540-48119-2_12","volume-title":"FM\u201999-Formal Methods","author":"Y. Kesten","year":"1999","unstructured":"Y. Kesten, A. Klein, A. Pnueli, and G. Raanan. A Perfecto Verification: Combining Model Checking with Deductive Analysis to Verify Real-Life Software. In J.M. Wing, J. Woodcock and J. Davies, editor, FM\u201999-Formal Methods, volume 1 of LNCS 1708, pages 173\u2013194. Springer-Verlag, 1999."}],"container-title":["Lecture Notes in Computer Science","FME 2002:Formal Methods\u2014Getting IT Right"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45614-7_10","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,5,11]],"date-time":"2023-05-11T22:05:08Z","timestamp":1683842708000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45614-7_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540439288","9783540456148"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/3-540-45614-7_10","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2002]]}}}