{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T04:19:26Z","timestamp":1743049166962,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":22,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540408284"},{"type":"electronic","value":"9783540452362"}],"license":[{"start":{"date-parts":[[2003,1,1]],"date-time":"2003-01-01T00:00:00Z","timestamp":1041379200000},"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":[[2003]]},"DOI":"10.1007\/978-3-540-45236-2_32","type":"book-chapter","created":{"date-parts":[[2010,6,25]],"date-time":"2010-06-25T20:08:38Z","timestamp":1277496518000},"page":"582-599","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Translation-Based Compositional Reasoning for Software Systems"],"prefix":"10.1007","author":[{"given":"Fei","family":"Xie","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"James C.","family":"Browne","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Robert P.","family":"Kurshan","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2003,9,25]]},"reference":[{"key":"32_CR1","unstructured":"Clarke, E.M., Emerson, E.A.: Design and synthesis of synchronization skeletons using branching time temporal logic. In: Logic of Programs Workshop (1981)"},{"key":"32_CR2","doi-asserted-by":"crossref","unstructured":"Quielle, J.P., Sifakis, J.: Specification and verification of concurrent systems in CESAR. In: 5th International Symposium on Programming (1982)","DOI":"10.1007\/3-540-11494-7_22"},{"key":"32_CR3","volume-title":"Model Checking","author":"E.M. Clarke","year":"1999","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. The MIT Press, Cambridge (1999)"},{"key":"32_CR4","doi-asserted-by":"crossref","unstructured":"Pnueli, A.: In transition from global to modular reasoning about programs. Logics and Models of Concurrent Systems (1985)","DOI":"10.1007\/978-3-642-82453-1_5"},{"key":"32_CR5","unstructured":"Alur, R., Henzinger, T.: Reactive modules. In: LICS (1996)"},{"key":"32_CR6","doi-asserted-by":"crossref","unstructured":"Abadi, M., Lamport, L.: Conjoining specifications. In: TOPLAS (1995)","DOI":"10.1145\/203095.201069"},{"key":"32_CR7","unstructured":"McMillan, K.L.: Amethodology for hardware verification using compositional model checking. Cadence TR (1999)"},{"key":"32_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"465","DOI":"10.1007\/3-540-45319-9_32","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"N. Amla","year":"2001","unstructured":"Amla, N., Emerson, E.A., Namjoshi, K.S., Trefler, R.: Assume-guarantee based compositional reasoning for synchronous timing diagrams. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol.\u00a02031, p. 465. Springer, Heidelberg (2001)"},{"key":"32_CR9","volume-title":"Concurrency Verification: Introduction to Compositional and Non-compositional Proof Methods","author":"W.P. Rover de","year":"2001","unstructured":"de Rover, W.P., de Boer, F., Hannemann, U., Hooman, J., Lakhnech, Y., Poel, M., Zwiers, J.: Concurrency Verification: Introduction to Compositional and Non-compositional Proof Methods. Cambridge Univ. Press, Cambridge (2001)"},{"key":"32_CR10","volume-title":"Executable UML: A Foundation for Model Driven Architecture","author":"S.J. Mellor","year":"2002","unstructured":"Mellor, S.J., Balcer, M.J.: Executable UML: A Foundation for Model Driven Architecture. Addison-Wesley, Reading (2002)"},{"key":"32_CR11","unstructured":"ITU: ITU-T Recommendation Z.100 (03\/93) - Specification and Description Language (SDL). ITU (1993)"},{"key":"32_CR12","volume-title":"Design and Validation of Computer Protocols","author":"G. Holzmann","year":"1991","unstructured":"Holzmann, G.: Design and Validation of Computer Protocols. Prentice-Hall, Englewood Cliffs (1991)"},{"key":"32_CR13","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4615-3190-6","volume-title":"Symbolic Model Checking","author":"K.L. McMillan","year":"1993","unstructured":"McMillan, K.L.: Symbolic Model Checking. Kluwer Academic Publishers, Dordrecht (1993)"},{"key":"32_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-61474-5_94","volume-title":"Computer Aided Verification","author":"R.H. Hardin","year":"1996","unstructured":"Hardin, R.H., Har\u2019El, Z., Kurshan, R.P.: COSPAN. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol.\u00a01102. Springer, Heidelberg (1996)"},{"key":"32_CR15","volume-title":"Computer-Aided Verification of Coordinating Processes: The Automata- Theoretic Approach","author":"R.P. Kurshan","year":"1994","unstructured":"Kurshan, R.P.: Computer-Aided Verification of Coordinating Processes: The Automata- Theoretic Approach. Princeton University Press, Princeton (1994)"},{"key":"32_CR16","volume-title":"Distributed Algorithms","author":"N. Lynch","year":"1996","unstructured":"Lynch, N.: Distributed Algorithms. Morgan Kaufmann Publishers, San Francisco (1996)"},{"key":"32_CR17","doi-asserted-by":"crossref","unstructured":"Kurshan, R.P., Merritt, M., Orda, A., Sachs, S.R.: Modeling asynchrony with a synchronous model. Formal Methods in System Design\u00a015(3) (1999)","DOI":"10.1023\/A:1008792918020"},{"key":"32_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"64","DOI":"10.1007\/3-540-45923-5_5","volume-title":"Fundamental Approaches to Software Engineering","author":"F. Xie","year":"2002","unstructured":"Xie, F., Browne, J.C.: Integrated state space reduction for model checking executable objectoriented software system designs. In: Kutsche, R.-D., Weber, H. (eds.) FASE 2002. LNCS, vol.\u00a02306, p. 64. Springer, Heidelberg (2002)"},{"key":"32_CR19","doi-asserted-by":"crossref","unstructured":"Xie, F., Browne, J.C.: Verified systems by composition from verified components. In: ESEC\/FSE (2003)","DOI":"10.1145\/940071.940109"},{"key":"32_CR20","doi-asserted-by":"crossref","unstructured":"Alpern, B., Schneider, F.: Defining liveness. Information Processing Letters\u00a021 (1985)","DOI":"10.1016\/0020-0190(85)90056-0"},{"key":"32_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"331","DOI":"10.1007\/3-540-45923-5_24","volume-title":"Fundamental Approaches to Software Engineering","author":"F. Xie","year":"2002","unstructured":"Xie, F., Levin, V., Browne, J.C.: ObjectCheck: a model checking tool for executable objectoriented software system designs. In: Kutsche, R.-D., Weber, H. (eds.) FASE 2002. LNCS, vol.\u00a02306, p. 331. Springer, Heidelberg (2002)"},{"key":"32_CR22","doi-asserted-by":"crossref","unstructured":"Hill, J., Szewczyk, R., Woo, A., Hollar, S., Culler, D., Pister, K.: System architecture directions for networked sensors. ASPLOS-IX (2000)","DOI":"10.1145\/378993.379006"}],"container-title":["Lecture Notes in Computer Science","FME 2003: Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-45236-2_32","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,1,23]],"date-time":"2020-01-23T13:09:43Z","timestamp":1579784983000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-45236-2_32"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003]]},"ISBN":["9783540408284","9783540452362"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-45236-2_32","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2003]]},"assertion":[{"value":"25 September 2003","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}